# HG changeset patch
# User bulwahn
# Date 1291362047 -3600
# Node ID 977c60b622f4674e793107db8d45a87d3b9b066b
# Parent  cdb34f393a7ef45b89fbe67fdb81513842863a28
adapting mutabelle

diff -r cdb34f393a7e -r 977c60b622f4 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Fri Dec 03 08:40:47 2010 +0100
@@ -55,7 +55,7 @@
 structure Mutabelle : MUTABELLE = 
 struct
 
-val testgen_name = Unsynchronized.ref "SML";
+val testgen_name = Unsynchronized.ref "random";
 
 fun all_unconcealed_thms_of thy =
   let
@@ -498,8 +498,11 @@
 
 fun is_executable thy insts th =
   ((Quickcheck.test_term 
-      ((Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) (ProofContext.init_global thy))
-      false (SOME (!testgen_name)) (preprocess thy insts (prop_of th));
+      (ProofContext.init_global thy
+      |> Config.put Quickcheck.size 1
+      |> Config.put Quickcheck.iterations 1
+      |> Config.put Quickcheck.tester (!testgen_name))
+      false (preprocess thy insts (prop_of th));
     Output.urgent_message "executable"; true) handle ERROR s =>
     (Output.urgent_message ("not executable: " ^ s); false));
 
@@ -507,9 +510,10 @@
  | qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter 
      (Output.urgent_message ("qc_recursive: " ^ string_of_int (length xs));
      ((x, pretty (the_default [] (fst (Quickcheck.test_term
-       ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter)
+       ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter
+        #> Config.put Quickcheck.tester (!testgen_name))
          (ProofContext.init_global usedthy))
-       false (SOME (!testgen_name)) (preprocess usedthy insts x))))) :: acc))
+       false (preprocess usedthy insts x))))) :: acc))
           handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc);
 
 
diff -r cdb34f393a7e -r 977c60b622f4 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Dec 03 08:40:47 2010 +0100
@@ -117,7 +117,7 @@
   TimeLimit.timeLimit (Time.fromSeconds (!Auto_Tools.time_limit))
       (fn _ =>
           case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
-              false (SOME quickcheck_generator, []) [t] of
+              false [] [t] of
             (NONE, _) => (NoCex, ([], NONE))
           | (SOME _, _) => (GenuineCex, ([], NONE))) ()
   handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Tools.time_limit)], NONE))
@@ -331,7 +331,7 @@
       (Quickcheck.test_goal_terms
         ((Config.put Quickcheck.finite_types true #>
           Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
-        false (SOME "random" , []))) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
+        false [])) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
   end
 
 fun is_executable_thm thy th = is_executable_term thy (prop_of th)