diff --git a/src/Dafny-VMC.dfy b/src/Dafny-VMC.dfy
index 36b96cf1..bd858c9f 100644
--- a/src/Dafny-VMC.dfy
+++ b/src/Dafny-VMC.dfy
@@ -16,10 +16,6 @@ module DafnyVMC {
     constructor {:extern} ()
   }
 
-/*   class DRandomExternUniform extends Coin.Interface.Trait, UniformPowerOfTwo.Implementation.Trait, Bernoulli.Implementation.Trait, Uniform.Implementation.TraitExtern, BernoulliExpNeg.Implementation.Trait, DiscreteGaussian.Implementation.Trait, DiscreteLaplace.Implementation.Trait {
-    constructor {:extern} ()
-  } */
-
   class DRandomExternUniform extends Coin.Interface.Trait, UniformPowerOfTwo.Implementation.TraitExtern, Bernoulli.Implementation.Trait, Uniform.Implementation.Trait, BernoulliExpNeg.Implementation.Trait, DiscreteGaussian.Implementation.Trait, DiscreteLaplace.Implementation.Trait {
     constructor {:extern} ()
   }
diff --git a/src/Distributions/Uniform/Implementation.dfy b/src/Distributions/Uniform/Implementation.dfy
index b19bd45f..49d3e1dd 100644
--- a/src/Distributions/Uniform/Implementation.dfy
+++ b/src/Distributions/Uniform/Implementation.dfy
@@ -32,19 +32,4 @@ module Uniform.Implementation {
       reveal Model.Sample();
     }
   }
-
-  method {:extern "DRandomUniform", "Uniform"} ExternUniformSample(n: nat) returns (u: nat)
-
-  trait {:termination false} TraitExtern extends Interface.Trait {
-    method UniformSample(n: nat) returns (u: nat)
-      modifies this
-      decreases *
-      requires n > 0
-      ensures u < n
-      ensures Model.Sample(n)(old(s)) == Monad.Result(u, s)
-    {
-      u := ExternUniformSample(n);
-      assume {:axiom} false; // assume correctness of extern implementation
-    }
-  }
 }