# HG changeset patch
# User bulwahn
# Date 1300468782 -3600
# Node ID 96327c90938912927e1aa24f7aae34a3f2324f19
# Parent  da92153d6dff8acd502e54a43addbd9aa1d4cb00
adapting mutabelle

diff -r da92153d6dff -r 96327c909389 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Fri Mar 18 18:19:42 2011 +0100
@@ -500,18 +500,18 @@
       |> Config.put Quickcheck.size 1
       |> Config.put Quickcheck.iterations 1
       |> Config.put Quickcheck.tester (!testgen_name))
-      (true, false) (preprocess thy insts (prop_of th));
+      (true, false) (preprocess thy insts (prop_of th), []);
     Output.urgent_message "executable"; true) handle ERROR s =>
     (Output.urgent_message ("not executable: " ^ s); false));
 
 fun qc_recursive usedthy [] insts sz qciter acc = rev acc
  | 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
+     ((x, pretty (the_default [] (Option.map fst (fst (Quickcheck.test_term
        ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter
         #> Config.put Quickcheck.tester (!testgen_name))
          (ProofContext.init_global usedthy))
-       (true, false) (preprocess usedthy insts x))))) :: acc))
+       (true, false) (preprocess usedthy insts x, [])))))) :: acc))
           handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc);
 
 
diff -r da92153d6dff -r 96327c909389 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 18 18:19:42 2011 +0100
@@ -122,7 +122,7 @@
   TimeLimit.timeLimit (seconds (!Auto_Tools.time_limit))
       (fn _ =>
           case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
-              (false, false) [] [t] of
+              (false, false) [] [(t, [])] of
             (NONE, _) => (NoCex, ([], NONE))
           | (SOME _, _) => (GenuineCex, ([], NONE))) ()
   handle TimeLimit.TimeOut =>
@@ -315,7 +315,7 @@
         ((Config.put Quickcheck.finite_types true #>
           Config.put Quickcheck.finite_type_size 1 #>
           Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
-        (false, false) [])) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
+        (false, false) [])) (map (rpair [] o 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)