src/HOL/Mutabelle/mutabelle.ML
changeset 45159 3f1d1ce024cb
parent 43883 aacbe67793c3
child 45428 aa35c9454a95
--- a/src/HOL/Mutabelle/mutabelle.ML	Sun Oct 16 21:49:47 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML	Mon Oct 17 10:19:01 2011 +0200
@@ -496,7 +496,7 @@
     val ctxt' = Proof_Context.init_global thy
       |> Config.put Quickcheck.size 1
       |> Config.put Quickcheck.iterations 1
-    val test = Quickcheck.test_term Exhaustive_Generators.compile_generator_expr ctxt' (true, false)
+    val test = Quickcheck_Common.test_term Exhaustive_Generators.compile_generator_expr ctxt' (true, false)
   in  
     case try test (preprocess thy insts (prop_of th), []) of
       SOME _ => (Output.urgent_message "executable"; true)