# HG changeset patch
# User bulwahn
# Date 1290422099 -3600
# Node ID d921c97bdbd8e0a942ca6fffd4791d56cc7a1be9
# Parent  7bdfc1d6b1433d0e6011fd96f717e8ef1b75501b
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle

diff -r 7bdfc1d6b143 -r d921c97bdbd8 src/HOL/Mutabelle/MutabelleExtra.thy
--- a/src/HOL/Mutabelle/MutabelleExtra.thy	Mon Nov 22 11:34:58 2010 +0100
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Mon Nov 22 11:34:59 2010 +0100
@@ -1,58 +1,144 @@
 theory MutabelleExtra
-imports Complex_Main SML_Quickcheck
-(*
-  "~/Downloads/Jinja/J/TypeSafe"
-  "~/Downloads/Jinja/J/Annotate"
-  (* FIXME "Example" *)
-  "~/Downloads/Jinja/J/execute_Bigstep"
-  "~/Downloads/Jinja/J/execute_WellType"
-  "~/Downloads/Jinja/JVM/JVMDefensive"
-  "~/Downloads/Jinja/JVM/JVMListExample"
-  "~/Downloads/Jinja/BV/BVExec"
-  "~/Downloads/Jinja/BV/LBVJVM"
-  "~/Downloads/Jinja/BV/BVNoTypeError"
-  "~/Downloads/Jinja/BV/BVExample"
-  "~/Downloads/Jinja/Compiler/TypeComp"
-*)
-(*"~/Downloads/NormByEval/NBE"*)
-uses "mutabelle.ML"
+imports Complex_Main
+(*  "~/repos/afp/thys/AVL-Trees/AVL"
+  "~/repos/afp/thys/BinarySearchTree/BinaryTree"
+  "~/repos/afp/thys/Huffman/Huffman"
+  "~/repos/afp/thys/List-Index/List_Index"
+  "~/repos/afp/thys/Matrix/Matrix"
+  "~/repos/afp/thys/NormByEval/NBE"
+  "~/repos/afp/thys/Polynomials/Polynomial"
+  "~/repos/afp/thys/Presburger-Automata/Presburger_Automata"
+  "~/repos/afp/thys/Abstract-Rewriting/Abstract_Rewriting"*)
+uses
+     "mutabelle.ML"
      "mutabelle_extra.ML"
 begin
 
-(* FIXME !?!?! *)
-ML {* val old_tr = !Output.Private_Hooks.tracing_fn *}
-ML {* val old_wr = !Output.Private_Hooks.writeln_fn *}
-ML {* val old_ur = !Output.Private_Hooks.urgent_message_fn *}
-ML {* val old_wa = !Output.Private_Hooks.warning_fn *}
+
+section {* configuration *}
 
-quickcheck_params [size = 5, iterations = 1000]
+ML {* val log_directory = "" *}
+
+
+quickcheck_params [quiet, finite_types = false, report = false, size = 5, iterations = 1000]
+
 (*
 nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
 refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
 *)
 ML {* Auto_Tools.time_limit := 10 *}
 
+ML {* val mtds = [
+  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
+  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "random",
+  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "small",
+  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "small"
+]
+*}
+
+ML {*
+fun mutation_testing_of (name, thy) =
+  (MutabelleExtra.random_seed := 1.0;
+  MutabelleExtra.thms_of false thy
+  |> MutabelleExtra.take_random 200
+  |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
+         @{theory} mtds thms (log_directory ^ "/" ^ name)))
+*}
+  
 
 text {* Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main. *}
 
+(*
 ML {*
-(*
+
       MutabelleExtra.random_seed := 1.0;
       MutabelleExtra.thms_of true @{theory Complex_Main}
       |> MutabelleExtra.take_random 1000000
       |> (fn thms => List.drop (thms, 1000))
       |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
-             @{theory} [MutabelleExtra.quickcheck_mtd "SML",
-                        MutabelleExtra.quickcheck_mtd "code"
+             @{theory} [
+                        MutabelleExtra.quickcheck_mtd "code",
+                        MutabelleExtra.smallcheck_mtd
                         (*MutabelleExtra.refute_mtd,
                         MutabelleExtra.nitpick_mtd*)] thms "/tmp/muta.out")
+
+ *}
 *)
+
+section {* Mutation testing Isabelle theories *}
+
+subsection {* List theory *}
+
+(*
+ML {*
+mutation_testing_of ("List", @{theory List})
  *}
+*)
+
+section {* Mutation testing AFP theories *}
+
+subsection {* AVL-Trees *}
+
+(*
+ML {*
+mutation_testing_of ("AVL-Trees", @{theory AVL})
+ *}
+*)
+
+subsection {* BinaryTree *}
+
+(*
+ML {*
+mutation_testing_of ("BinaryTree", @{theory BinaryTree})
+ *}
+*)
+
+subsection {* Huffman *}
+
+(*
+ML {*
+mutation_testing_of ("Huffman", @{theory Huffman})
+ *}
+*)
 
-(* FIXME !?!?! *)
-ML {* Output.Private_Hooks.tracing_fn := old_tr *}
-ML {* Output.Private_Hooks.writeln_fn := old_wr *}
-ML {* Output.Private_Hooks.urgent_message_fn := old_ur *}
-ML {* Output.Private_Hooks.warning_fn := old_wa *}
+subsection {* List_Index *}
+
+(*
+ML {*
+mutation_testing_of ("List_Index", @{theory List_Index})
+ *}
+*)
+
+subsection {* Matrix *}
+
+(*
+ML {*
+mutation_testing_of ("Matrix", @{theory Matrix})
+ *}
+*)
+
+subsection {* NBE *}
+
+(*
+ML {*
+mutation_testing_of ("NBE", @{theory NBE})
+ *}
+*)
+
+subsection {* Polynomial *}
+
+(*
+ML {*
+mutation_testing_of ("Polynomial", @{theory Polynomial})
+ *}
+*)
+
+subsection {* Presburger Automata *}
+
+(*
+ML {*
+mutation_testing_of ("Presburger_Automata", @{theory Presburger_Automata})
+ *}
+*)
 
 end
diff -r 7bdfc1d6b143 -r d921c97bdbd8 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Mon Nov 22 11:34:58 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Mon Nov 22 11:34:59 2010 +0100
@@ -498,7 +498,7 @@
 
 fun is_executable thy insts th =
   ((Quickcheck.test_term
-      (Context.proof_map (Quickcheck.map_test_params (apfst (K (1, 1)))) (ProofContext.init_global thy))
+      ((Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) (ProofContext.init_global thy))
       (SOME (!testgen_name)) (preprocess thy insts (prop_of th));
     Output.urgent_message "executable"; true) handle ERROR s =>
     (Output.urgent_message ("not executable: " ^ s); false));
@@ -507,7 +507,7 @@
  | 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
-       (Context.proof_map (Quickcheck.map_test_params (apfst (K (sz, qciter))))
+       ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter)
          (ProofContext.init_global usedthy))
        (SOME (!testgen_name)) (preprocess usedthy insts x))))) :: acc))
           handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc);
diff -r 7bdfc1d6b143 -r d921c97bdbd8 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Nov 22 11:34:58 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Nov 22 11:34:59 2010 +0100
@@ -8,7 +8,7 @@
 
 val take_random : int -> 'a list -> 'a list
 
-datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
+datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
 type timing = (string * int) list
 
 type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
@@ -20,7 +20,10 @@
 type entry = string * bool * subentry list
 type report = entry list
 
-val quickcheck_mtd : string -> mtd
+val quickcheck_mtd : (Proof.context -> Proof.context) -> string -> mtd
+
+val solve_direct_mtd : mtd
+val try_mtd : mtd
 (*
 val refute_mtd : mtd
 val nitpick_mtd : mtd
@@ -45,15 +48,17 @@
 
 
 (* mutation options *)
-val max_mutants = 4
-val num_mutations = 1
+(*val max_mutants = 4
+val num_mutations = 1*)
 (* soundness check: *)
-(*val max_mutants = 1
-val num_mutations = 0*)
+val max_mutants =  10
+val num_mutations = 1
 
 (* quickcheck options *)
 (*val quickcheck_generator = "SML"*)
 
+(* Another Random engine *)
+
 exception RANDOM;
 
 fun rmod x y = x - y * Real.realFloor (x / y);
@@ -73,7 +78,26 @@
   if h < l orelse l < 0 then raise RANDOM
   else l + Real.floor (rmod (random ()) (real (h - l + 1)));
 
-datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
+fun take_random 0 _ = []
+  | take_random _ [] = []
+  | take_random n xs =
+    let val j = random_range 0 (length xs - 1) in
+      Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
+    end
+  
+(* possible outcomes *)
+
+datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
+
+fun string_of_outcome GenuineCex = "GenuineCex"
+  | string_of_outcome PotentialCex = "PotentialCex"
+  | string_of_outcome NoCex = "NoCex"
+  | string_of_outcome Donno = "Donno"
+  | string_of_outcome Timeout = "Timeout"
+  | string_of_outcome Error = "Error"
+  | string_of_outcome Solved = "Solved"
+  | string_of_outcome Unsolved = "Unsolved"
+
 type timing = (string * int) list
 
 type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
@@ -85,25 +109,49 @@
 type entry = string * bool * subentry list
 type report = entry list
 
-fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
-  | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T)
+(* possible invocations *)
 
-fun preprocess thy insts t = Object_Logic.atomize_term thy
- (map_types (inst_type insts) (Mutabelle.freeze t));
+(** quickcheck **)
 
-fun invoke_quickcheck quickcheck_generator thy t =
+fun invoke_quickcheck change_options quickcheck_generator thy t =
   TimeLimit.timeLimit (Time.fromSeconds (!Auto_Tools.time_limit))
       (fn _ =>
-          case Quickcheck.test_term (ProofContext.init_global thy)
-              (SOME quickcheck_generator) (preprocess thy [] t) of
-            (NONE, (time_report, report)) => (NoCex, (time_report, report))
-          | (SOME _, (time_report, report)) => (GenuineCex, (time_report, report))) ()
+          case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
+              (SOME quickcheck_generator, []) [t] of
+            (NONE, _) => (NoCex, ([], NONE))
+          | (SOME _, _) => (GenuineCex, ([], NONE))) ()
   handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Tools.time_limit)], NONE))
 
-fun quickcheck_mtd quickcheck_generator =
-  ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck quickcheck_generator)
+fun quickcheck_mtd change_options quickcheck_generator =
+  ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)
+
+(** solve direct **)
+ 
+fun invoke_solve_direct thy t =
+  let
+    val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) 
+  in
+    case Solve_Direct.solve_direct false state of
+      (true, _) => (Solved, ([], NONE))
+    | (false, _) => (Unsolved, ([], NONE))
+  end
 
-  (*
+val solve_direct_mtd = ("solve_direct", invoke_solve_direct) 
+
+(** try **)
+
+fun invoke_try thy t =
+  let
+    val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) 
+  in
+    case Try.invoke_try NONE state of
+      true => (Solved, ([], NONE))
+    | false => (Unsolved, ([], NONE))
+  end
+
+val try_mtd = ("try", invoke_try)
+
+(*
 fun invoke_refute thy t =
   let
     val res = MyRefute.refute_term thy [] t
@@ -185,6 +233,8 @@
 val nitpick_mtd = ("nitpick", invoke_nitpick)
 *)
 
+(* filtering forbidden theorems and mutants *)
+
 val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]
 
 val forbidden =
@@ -200,7 +250,6 @@
   (@{const_name "top_fun_inst.top_fun"}, "'a"),
   (@{const_name "Pure.term"}, "'a"),
   (@{const_name "top_class.top"}, "'a"),
-  (@{const_name "HOL.equal"}, "'a"),
   (@{const_name "Quotient.Quot_True"}, "'a")(*,
   (@{const_name "uminus"}, "'a"),
   (@{const_name "Nat.size"}, "'a"),
@@ -211,7 +260,7 @@
   "nibble"]
 
 val forbidden_consts =
- [@{const_name nibble_pair_of_char}]
+ [@{const_name nibble_pair_of_char}, @{const_name "TYPE"}]
 
 fun is_forbidden_theorem (s, th) =
   let val consts = Term.add_const_names (prop_of th) [] in
@@ -220,7 +269,8 @@
     length (space_explode "." s) <> 2 orelse
     String.isPrefix "type_definition" (List.last (space_explode "." s)) orelse
     String.isSuffix "_def" s orelse
-    String.isSuffix "_raw" s
+    String.isSuffix "_raw" s orelse
+    String.isPrefix "term_of" (List.last (space_explode "." s))
   end
 
 val forbidden_mutant_constnames =
@@ -235,23 +285,54 @@
  @{const_name "top_fun_inst.top_fun"},
  @{const_name "Pure.term"},
  @{const_name "top_class.top"},
- @{const_name "HOL.equal"},
- @{const_name "Quotient.Quot_True"}]
+ (*@{const_name "HOL.equal"},*)
+ @{const_name "Quotient.Quot_True"}
+ (*@{const_name "==>"}, @{const_name "=="}*)]
+
+val forbidden_mutant_consts =
+  [
+   (@{const_name "Groups.zero_class.zero"}, @{typ "prop => prop => prop"}),
+   (@{const_name "Groups.one_class.one"}, @{typ "prop => prop => prop"}),
+   (@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}),
+   (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}),
+   (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}),
+   (@{const_name "Rings.inverse_class.divide"}, @{typ "prop => prop => prop"}),
+   (@{const_name "Lattices.semilattice_inf_class.inf"}, @{typ "prop => prop => prop"}),
+   (@{const_name "Lattices.semilattice_sup_class.sup"}, @{typ "prop => prop => prop"}),
+   (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
+   (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}),
+   (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}),
+   (@{const_name "Divides.div_class.mod"}, @{typ "prop => prop => prop"}),
+   (@{const_name "Divides.div_class.div"}, @{typ "prop => prop => prop"}),
+   (@{const_name "GCD.gcd_class.gcd"}, @{typ "prop => prop => prop"}),
+   (@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}),
+   (@{const_name "Orderings.bot_class.bot"}, @{typ "bool => prop"}),
+   (@{const_name "Groups.one_class.one"}, @{typ "bool => prop"}),
+   (@{const_name "Groups.zero_class.zero"},@{typ "bool => prop"})]
 
 fun is_forbidden_mutant t =
   let
-    val consts = Term.add_const_names t []
+    val const_names = Term.add_const_names t []
+    val consts = Term.add_consts t []
   in
-    exists (String.isPrefix "Nitpick") consts orelse
-    exists (String.isSubstring "_sumC") consts orelse
-    exists (member (op =) forbidden_mutant_constnames) consts
+    exists (String.isPrefix "Nitpick") const_names orelse
+    exists (String.isSubstring "_sumC") const_names orelse
+    exists (member (op =) forbidden_mutant_constnames) const_names orelse
+    exists (member (op =) forbidden_mutant_consts) consts
   end
 
+(* executable via quickcheck *)
+
 fun is_executable_term thy t =
-  can (TimeLimit.timeLimit (seconds 2.0)
-    (Quickcheck.test_term
-      (Context.proof_map (Quickcheck.map_test_params (apfst (K (1, 0)))) (ProofContext.init_global thy))
-      (SOME "SML"))) (preprocess thy [] t)
+  let
+    val ctxt = ProofContext.init_global thy
+  in
+    can (TimeLimit.timeLimit (seconds 2.0)
+      (Quickcheck.test_goal_terms
+        ((Config.put Quickcheck.finite_types true #>
+          Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
+        (SOME "random" , []))) (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)
 
@@ -267,44 +348,47 @@
 
 val count = length oo filter o equal
 
-fun take_random 0 _ = []
-  | take_random _ [] = []
-  | take_random n xs =
-    let val j = random_range 0 (length xs - 1) in
-      Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
-    end
-
 fun cpu_time description f =
   let
     val start = start_timing ()
     val result = Exn.capture f ()
     val time = Time.toMilliseconds (#cpu (end_timing start))
   in (Exn.release result, (description, time)) end
-
+(*
+fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
+  let
+    val _ = Output.urgent_message ("Invoking " ^ mtd_name)
+    val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => invoke_mtd thy t
+      handle ERROR s => (tracing s; (Error, ([], NONE))))
+    val _ = Output.urgent_message (" Done")
+  in (res, (time :: timing, reports)) end
+*)  
 fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
   let
     val _ = Output.urgent_message ("Invoking " ^ mtd_name)
-    val ((res, (timing, reports)), time) = cpu_time "total time"
-      (fn () => case try (invoke_mtd thy) t of
+    val (res, (timing, reports)) = (*cpu_time "total time"
+      (fn () => *)case try (invoke_mtd thy) t of
           SOME (res, (timing, reports)) => (res, (timing, reports))
         | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
-           (Error , ([], NONE))))
+           (Error, ([], NONE)))
     val _ = Output.urgent_message (" Done")
-  in (res, (time :: timing, reports)) end
+  in (res, (timing, reports)) end
 
 (* theory -> term list -> mtd -> subentry *)
-(*
+
 fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) =
   let
-     val res = map (safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
+     val res = map (fst o safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
   in
     (mtd_name, count GenuineCex res, count PotentialCex res, count NoCex res,
      count Donno res, count Timeout res, count Error res)
   end
 
+(* creating entries *)
+
 fun create_entry thy thm exec mutants mtds =
   (Thm.get_name_hint thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
-*)
+
 fun create_detailed_entry thy thm exec mutants mtds =
   let
     fun create_mutant_subentry mutant = (mutant,
@@ -318,13 +402,14 @@
 fun mutate_theorem create_entry thy mtds thm =
   let
     val exec = is_executable_thm thy thm
-    val _ = Output.urgent_message (if exec then "EXEC" else "NOEXEC")
+    val _ = Output.tracing (if exec then "EXEC" else "NOEXEC")
     val mutants =
           (if num_mutations = 0 then
              [Thm.prop_of thm]
            else
              Mutabelle.mutate_mix (Thm.prop_of thm) thy comms forbidden
                                   num_mutations)
+             |> tap (fn muts => tracing ("mutants: " ^ string_of_int (length muts)))
              |> filter_out is_forbidden_mutant
     val mutants =
       if exec then
@@ -344,6 +429,7 @@
           |> map Mutabelle.freeze |> map freezeT
 (*          |> filter (not o is_forbidden_mutant) *)
           |> List.mapPartial (try (Sign.cert_term thy))
+          |> List.filter (is_some o try (cterm_of thy))
     val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
   in
     create_entry thy thm exec mutants mtds
@@ -352,13 +438,6 @@
 (* theory -> mtd list -> thm list -> report *)
 val mutate_theorems = map ooo mutate_theorem
 
-fun string_of_outcome GenuineCex = "GenuineCex"
-  | string_of_outcome PotentialCex = "PotentialCex"
-  | string_of_outcome NoCex = "NoCex"
-  | string_of_outcome Donno = "Donno"
-  | string_of_outcome Timeout = "Timeout"
-  | string_of_outcome Error = "Error"
-
 fun string_of_mutant_subentry thy thm_name (t, results) =
   "mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^
   space_implode "; "
@@ -378,12 +457,12 @@
         cat_lines (map (fn (size, [report]) =>
           "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))
     fun string_of_mtd_result (mtd_name, (outcome, (timing, reports))) =
-      mtd_name ^ ": " ^ string_of_outcome outcome ^ "; " ^
-      space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing)
+      mtd_name ^ ": " ^ string_of_outcome outcome
+      (*" with time " ^ " (" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"*)
       (*^ "\n" ^ string_of_reports reports*)
   in
     "mutant of " ^ thm_name ^ ":\n"
-    ^ unyxml (Syntax.string_of_term_global thy t) ^ "\n" ^ cat_lines (map string_of_mtd_result results)
+    ^ unyxml (Syntax.string_of_term_global thy t) ^ "\n" ^ space_implode "; " (map string_of_mtd_result results)
   end
 
 fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) = 
@@ -394,8 +473,7 @@
 fun theoryfile_string_of_mutant_subentry thy thm_name (i, (t, results)) =
   "lemma " ^ thm_name ^ "_" ^ string_of_int (i + 1) ^ ":\n" ^
   "\"" ^ unyxml (Syntax.string_of_term_global thy t) ^
-  "\" \nquickcheck[generator = SML]\nquickcheck[generator = predicate_compile_wo_ff]\n" ^
-  "quickcheck[generator = predicate_compile_ff_nofs]\noops\n"
+  "\" \nquickcheck\noops\n"
 
 fun theoryfile_string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
   "subsubsection {* mutants of " ^ thm_name ^ " *}\n\n" ^
@@ -409,10 +487,12 @@
   Int.toString potential_cex ^ "= " ^ Int.toString no_cex ^ "- " ^
   Int.toString donno ^ "? " ^ Int.toString timeout ^ "T " ^
   Int.toString error ^ "!"
+
 (* entry -> string *)
 fun string_for_entry (thm_name, exec, subentries) =
   thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ":\n" ^
   cat_lines (map string_for_subentry subentries) ^ "\n"
+
 (* report -> string *)
 fun string_for_report report = cat_lines (map string_for_entry report)
 
@@ -424,15 +504,16 @@
 fun mutate_theorems_and_write_report thy mtds thms file_name =
   let
     val _ = Output.urgent_message "Starting Mutabelle..."
-    val Quickcheck.Test_Params test_params = Quickcheck.test_params_of (ProofContext.init_global thy)
+    val ctxt = ProofContext.init_global thy
     val path = Path.explode file_name
     (* for normal report: *)
-    (*val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)*)
-    (*for detailled report: *)
-    val (gen_create_entry, gen_string_for_entry) =
-      (create_detailed_entry, string_of_detailed_entry thy)
-    val (gen_create_entry, gen_string_for_entry) =
-      (create_detailed_entry, theoryfile_string_of_detailed_entry thy)
+    (*
+    val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)
+    *)
+    (* for detailled report: *)
+    val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, string_of_detailed_entry thy)
+    (* for theory creation: *)
+    (*val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, theoryfile_string_of_detailed_entry thy)*)
   in
     File.write path (
     "Mutation options = "  ^
@@ -440,8 +521,8 @@
       "; num_mutations: " ^ string_of_int num_mutations ^ "\n" ^
     "QC options = " ^
       (*"quickcheck_generator: " ^ quickcheck_generator ^ ";*)
-      "size: " ^ string_of_int (#size test_params) ^
-      "; iterations: " ^ string_of_int (#iterations test_params) ^ "\n");
+      "size: " ^ string_of_int (Config.get ctxt Quickcheck.size) ^
+      "; iterations: " ^ string_of_int (Config.get ctxt Quickcheck.iterations) ^ "\n");
     map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy mtds) thms;
     ()
   end