moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms

--- 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)

--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Oct 16 21:49:47 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Oct 17 10:19:01 2011 +0200
@@ -122,8 +122,11 @@
   TimeLimit.timeLimit (seconds (!Try.auto_time_limit))
       (fn _ =>
           let
-            val SOME [result] = Quickcheck.test_goal_terms (change_options (Proof_Context.init_global thy))
-              (false, false) [] [(t, [])]
+            val ctxt' = change_options (Proof_Context.init_global thy)
+            val [result] = case Quickcheck.active_testers ctxt' of
+              [] => error "No active testers for quickcheck"
+            | [tester] => tester ctxt' (false, false) [] [(t, [])]
+            | _ => error "Multiple active testers for quickcheck"
           in
             case Quickcheck.counterexample_of result of 
               NONE => (NoCex, Quickcheck.timings_of result)
@@ -317,11 +320,12 @@
     val ctxt = Proof_Context.init_global thy
   in
     can (TimeLimit.timeLimit (seconds 2.0)
-      (Quickcheck.test_goal_terms
+      (Quickcheck.test_terms
         ((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 (rpair [] o 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)

--- a/src/HOL/Quickcheck.thy	Sun Oct 16 21:49:47 2011 +0200
+++ b/src/HOL/Quickcheck.thy	Mon Oct 17 10:19:01 2011 +0200
@@ -144,6 +144,12 @@
 no_notation fcomp (infixl "\<circ>>" 60)
 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
+subsection {* Tester SML-inductive based on the SML code generator *}
+
+setup {*
+  Context.theory_map (Quickcheck.add_tester ("SML_inductive",
+    (Inductive_Codegen.active, Quickcheck_Common.generator_test_goal_terms Inductive_Codegen.test_term)));
+*}
 
 subsection {* The Random-Predicate Monad *} 
 

--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Sun Oct 16 21:49:47 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Oct 17 10:19:01 2011 +0200
@@ -488,7 +488,7 @@
       thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') []
   end;
 
-val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr;
+val test_goals = Quickcheck_Common.generator_test_goal_terms compile_generator_expr;
   
 (* setup *)
 

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Oct 16 21:49:47 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Oct 17 10:19:01 2011 +0200
@@ -462,9 +462,9 @@
 fun test_goals ctxt (limit_time, is_interactive) insts goals =
   if (not (getenv "ISABELLE_GHC" = "")) then
     let
-      val correct_inst_goals = Quickcheck.instantiate_goals ctxt insts goals
+      val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
     in
-      Quickcheck.collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
+      Quickcheck_Common.collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
     end
   else
     (if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message

--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sun Oct 16 21:49:47 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Oct 17 10:19:01 2011 +0200
@@ -11,6 +11,13 @@
     -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context 
   val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
     -> (string * sort -> string * sort) option
+  val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
+    -> (typ option * (term * term list)) list list
+  val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
+  type compile_generator =
+    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
+  val generator_test_goal_terms : compile_generator -> Proof.context -> bool * bool
+    -> (string * typ) list -> (term * term list) list -> Quickcheck.result list
   val ensure_sort_datatype:
     ((sort * sort) * sort) * (Datatype.config -> Datatype.descr -> (string * sort) list
       -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory)
@@ -20,6 +27,7 @@
      -> Proof.context -> (term * term list) list -> term
   val mk_fun_upd : typ -> typ -> term * term -> term -> term
   val post_process_term : term -> term
+  val test_term : compile_generator -> Proof.context -> bool * bool -> term * term list -> Quickcheck.result
 end;
 
 structure Quickcheck_Common : QUICKCHECK_COMMON =
@@ -35,7 +43,222 @@
   | strip_imp A = ([], A)
 
 fun mk_undefined T = Const(@{const_name undefined}, T)
+
+(* testing functions: testing with increasing sizes (and cardinalities) *)
+
+type compile_generator =
+  Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
+
+fun check_test_term t =
+  let
+    val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
+      error "Term to be tested contains type variables";
+    val _ = null (Term.add_vars t []) orelse
+      error "Term to be tested contains schematic variables";
+  in () end
+
+fun cpu_time description e =
+  let val ({cpu, ...}, result) = Timing.timing e ()
+  in (result, (description, Time.toMilliseconds cpu)) end
+
+fun test_term compile ctxt (limit_time, is_interactive) (t, eval_terms) =
+  let
+    val _ = check_test_term t
+    val names = Term.add_free_names t []
+    val current_size = Unsynchronized.ref 0
+    val current_result = Unsynchronized.ref Quickcheck.empty_result 
+    fun excipit () =
+      "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
+    fun with_size test_fun k =
+      if k > Config.get ctxt Quickcheck.size then
+        NONE
+      else
+        let
+          val _ = Quickcheck.message ctxt ("Test data size: " ^ string_of_int k)
+          val _ = current_size := k
+          val ((result, report), timing) =
+            cpu_time ("size " ^ string_of_int k) (fn () => test_fun [1, k - 1])
+          val _ = Quickcheck.add_timing timing current_result
+          val _ = Quickcheck.add_report k report current_result
+        in
+          case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q
+        end;
+  in
+    (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)(
+      let
+        val (test_fun, comp_time) = cpu_time "quickcheck compilation"
+          (fn () => compile ctxt [(t, eval_terms)]);
+        val _ = Quickcheck.add_timing comp_time current_result
+        val (response, exec_time) =
+          cpu_time "quickcheck execution" (fn () => with_size test_fun 1)
+        val _ = Quickcheck.add_response names eval_terms response current_result
+        val _ = Quickcheck.add_timing exec_time current_result
+      in !current_result end)
+(*    (fn () => (message (excipit ()); !current_result)) ()*)
+  end;
+
+fun validate_terms ctxt ts =
+  let
+    val _ = map check_test_term ts
+    val size = Config.get ctxt Quickcheck.size
+    val (test_funs, comp_time) = cpu_time "quickcheck batch compilation"
+      (fn () => Quickcheck.mk_batch_validator ctxt ts) 
+    fun with_size tester k =
+      if k > size then true
+      else if tester k then with_size tester (k + 1) else false
+    val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
+        Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout))
+              (fn () => with_size test_fun 1) ()
+             handle TimeLimit.TimeOut => true)) test_funs)
+  in
+    (results, [comp_time, exec_time])
+  end
   
+fun test_terms ctxt ts =
+  let
+    val _ = map check_test_term ts
+    val size = Config.get ctxt Quickcheck.size
+    val namess = map (fn t => Term.add_free_names t []) ts
+    val (test_funs, comp_time) =
+      cpu_time "quickcheck batch compilation" (fn () => Quickcheck.mk_batch_tester ctxt ts) 
+    fun with_size tester k =
+      if k > size then NONE
+      else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1)
+    val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
+        Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout))
+              (fn () => with_size test_fun 1) ()
+             handle TimeLimit.TimeOut => NONE)) test_funs)
+  in
+    (Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results,
+      [comp_time, exec_time])
+  end
+
+
+fun test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) ts =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val (ts', eval_terms) = split_list ts
+    val _ = map check_test_term ts'
+    val names = Term.add_free_names (hd ts') []
+    val Ts = map snd (Term.add_frees (hd ts') [])
+    val current_result = Unsynchronized.ref Quickcheck.empty_result
+    fun test_card_size test_fun (card, size) =
+      (* FIXME: why decrement size by one? *)
+      let
+        val (ts, timing) =
+          cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
+            (fn () => fst (test_fun [card, size - 1]))
+        val _ = Quickcheck.add_timing timing current_result
+      in
+        Option.map (pair card) ts
+      end
+    val enumeration_card_size =
+      if forall (fn T => Sign.of_sort thy (T,  ["Enum.enum"])) Ts then
+        (* size does not matter *)
+        map (rpair 0) (1 upto (length ts))
+      else
+        (* size does matter *)
+        map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt Quickcheck.size))
+        |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
+  in
+    (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)(
+      let
+        val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => compile ctxt ts)
+        val _ = Quickcheck.add_timing comp_time current_result     
+        val _ = case get_first (test_card_size test_fun) enumeration_card_size of
+          SOME (card, ts) => Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME ts) current_result
+        | NONE => ()
+      in !current_result end)
+      (*(fn () => (message "Quickcheck ran out of time"; !current_result)) ()*)
+  end
+
+fun get_finite_types ctxt =
+  fst (chop (Config.get ctxt Quickcheck.finite_type_size)
+    (map (Type o rpair []) ["Enum.finite_1", "Enum.finite_2", "Enum.finite_3",
+     "Enum.finite_4", "Enum.finite_5"]))
+
+exception WELLSORTED of string
+
+fun monomorphic_term thy insts default_T =
+  let
+    fun subst (T as TFree (v, S)) =
+      let
+        val T' = AList.lookup (op =) insts v
+          |> the_default default_T
+      in if Sign.of_sort thy (T', S) then T'
+        else raise (WELLSORTED ("For instantiation with default_type " ^
+          Syntax.string_of_typ_global thy default_T ^
+          ":\n" ^ Syntax.string_of_typ_global thy T' ^
+          " to be substituted for variable " ^
+          Syntax.string_of_typ_global thy T ^ " does not have sort " ^
+          Syntax.string_of_sort_global thy S))
+      end
+      | subst T = T;
+  in (map_types o map_atyps) subst end;
+
+datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list
+
+fun instantiate_goals lthy insts goals =
+  let
+    fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms)
+    val thy = Proof_Context.theory_of lthy
+    val default_insts =
+      if Config.get lthy Quickcheck.finite_types then (get_finite_types lthy) else (Quickcheck.default_type lthy)
+    val inst_goals =
+      map (fn (check_goal, eval_terms) =>
+        if not (null (Term.add_tfree_names check_goal [])) then
+          map (fn T =>
+            (pair (SOME T) o Term o apfst (Object_Logic.atomize_term thy))
+              (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms))
+              handle WELLSORTED s => (SOME T, Wellsorted_Error s)) default_insts
+        else
+          [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) goals
+    val error_msg =
+      cat_lines
+        (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
+    fun is_wellsorted_term (T, Term t) = SOME (T, t)
+      | is_wellsorted_term (_, Wellsorted_Error s) = NONE
+    val correct_inst_goals =
+      case map (map_filter is_wellsorted_term) inst_goals of
+        [[]] => error error_msg
+      | xs => xs
+    val _ = if Config.get lthy Quickcheck.quiet then () else warning error_msg
+  in
+    correct_inst_goals
+  end
+
+fun collect_results f [] results = results
+  | collect_results f (t :: ts) results =
+    let
+      val result = f t
+    in
+      if Quickcheck.found_counterexample result then
+        (result :: results)
+      else
+        collect_results f ts (result :: results)
+    end  
+
+fun add_equation_eval_terms (t, eval_terms) =
+  case try HOLogic.dest_eq (snd (strip_imp t)) of
+    SOME (lhs, rhs) => (t, eval_terms @ [rhs, lhs])
+  | NONE => (t, eval_terms)
+
+fun generator_test_goal_terms compile ctxt (limit_time, is_interactive) insts goals =
+  let
+    fun test_term' goal =
+      case goal of
+        [(NONE, t)] => test_term compile ctxt (limit_time, is_interactive) t
+      | ts => test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) (map snd ts)
+    val goals' = instantiate_goals ctxt insts goals
+      |> map (map (apsnd add_equation_eval_terms))
+  in
+    if Config.get ctxt Quickcheck.finite_types then
+      collect_results test_term' goals' []
+    else
+      collect_results (test_term compile ctxt (limit_time, is_interactive))
+        (maps (map snd) goals') []
+  end;
+
 (* defining functions *)
 
 fun pat_completeness_auto ctxt =

--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sun Oct 16 21:49:47 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Oct 17 10:19:01 2011 +0200
@@ -438,7 +438,7 @@
       end
   end;
 
-val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr;
+val test_goals = Quickcheck_Common.generator_test_goal_terms compile_generator_expr;
   
 (** setup **)
 

--- a/src/HOL/Tools/inductive_codegen.ML	Sun Oct 16 21:49:47 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon Oct 17 10:19:01 2011 +0200
@@ -10,8 +10,8 @@
   val poke_test_fn: (int * int * int -> term list option) -> unit
   val test_term: Proof.context -> (term * term list) list -> int list ->
     term list option * Quickcheck.report option
+  val active : bool Config.T
   val setup: theory -> theory
-  val quickcheck_setup: theory -> theory
 end;
 
 structure Inductive_Codegen : INDUCTIVE_CODEGEN =
@@ -862,12 +862,12 @@
       NONE => deepen bound f (i + 1)
     | SOME x => SOME x);
 
-val active = Attrib.setup_config_bool @{binding quickcheck_inductive_SML_active} (K false);
+val active = Attrib.setup_config_bool @{binding quickcheck_SML_inductive_active} (K false);
     
-val depth_bound = Attrib.setup_config_int @{binding ind_quickcheck_depth} (K 10);
-val depth_start = Attrib.setup_config_int @{binding ind_quickcheck_depth_start} (K 1);
-val random_values = Attrib.setup_config_int @{binding ind_quickcheck_random} (K 5);
-val size_offset = Attrib.setup_config_int @{binding ind_quickcheck_size_offset} (K 0);
+val depth_bound = Attrib.setup_config_int @{binding quickcheck_ind_depth} (K 10);
+val depth_start = Attrib.setup_config_int @{binding quickcheck_ind_depth_start} (K 1);
+val random_values = Attrib.setup_config_int @{binding quickcheck_ind_random} (K 5);
+val size_offset = Attrib.setup_config_int @{binding quickcheck_ind_size_offset} (K 0);
 
 fun test_term ctxt [(t, [])] =
       let
@@ -926,9 +926,4 @@
   | test_term ctxt _ =
       error "Compilation of multiple instances is not supported by tester SML_inductive";
 
-val test_goal = Quickcheck.generator_test_goal_terms test_term;
-
-val quickcheck_setup =
-  Context.theory_map (Quickcheck.add_tester ("SML_inductive", (active, test_goal)));
-
 end;

--- a/src/Tools/quickcheck.ML	Sun Oct 16 21:49:47 2011 +0200
+++ b/src/Tools/quickcheck.ML	Mon Oct 17 10:19:01 2011 +0200
@@ -29,6 +29,7 @@
   val test_params_of : Proof.context -> test_params
   val map_test_params : (typ list * expectation -> typ list * expectation)
     -> Context.generic -> Context.generic
+  val default_type : Proof.context -> typ list
   datatype report = Report of
     { iterations : int, raised_match_errors : int,
       satisfied_assms : int list, positive_concl_tests : int }
@@ -40,7 +41,10 @@
       timings : (string * int) list,
       reports : (int * report) list}
   val empty_result : result
+  val found_counterexample : result -> bool
   val add_timing : (string * int) -> result Unsynchronized.ref -> unit
+  val add_response : string list -> term list -> term list option -> result Unsynchronized.ref -> unit
+  val add_report : int -> report option -> result Unsynchronized.ref -> unit
   val counterexample_of : result -> (string * term) list option
   val timings_of : result -> (string * int) list
   (* registering testers & generators *) 
@@ -54,23 +58,15 @@
     string * (Proof.context -> term list -> (int -> bool) list)
       -> Context.generic -> Context.generic
   (* basic operations *)
-  type compile_generator =
-    Proof.context -> (term * term list) list -> int list -> term list option * report option
-  val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a  
-  val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
-    -> (typ option * (term * term list)) list list
-  val collect_results : ('a -> result) -> 'a list -> result list -> result list
-  val generator_test_goal_terms : compile_generator ->
-    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
+  val message : Proof.context -> string -> unit
+  val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a
   (* testing terms and proof states *)
-  val test_term: compile_generator -> Proof.context -> bool * bool -> term * term list -> result
-  val test_goal_terms :
+  val mk_batch_validator : Proof.context -> term list -> (int -> bool) list option
+  val mk_batch_tester : Proof.context -> term list -> (int -> term list option) list option
+  val active_testers : Proof.context -> tester list
+  val test_terms :
     Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list option
   val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
-  (* testing a batch of terms *)
-  val test_terms:
-    Proof.context -> term list -> (string * term) list option list option * (string * int) list
-  val validate_terms: Proof.context -> term list -> bool list option * (string * int) list
 end;
 
 structure Quickcheck : QUICKCHECK =
@@ -119,14 +115,15 @@
 
 fun timings_of (Result r) = #timings r
 
-fun set_reponse names eval_terms (SOME ts) (Result r) =
+fun set_response names eval_terms (SOME ts) (Result r) =
   let
     val (ts1, ts2) = chop (length names) ts
+    val (eval_terms', _) = chop (length ts2) eval_terms
   in
-    Result {counterexample = SOME (names ~~ ts1), evaluation_terms = SOME (eval_terms ~~ ts2),
+    Result {counterexample = SOME (names ~~ ts1), evaluation_terms = SOME (eval_terms' ~~ ts2),
       timings = #timings r, reports = #reports r}
   end
-  | set_reponse _ _ NONE result = result
+  | set_response _ _ NONE result = result
 
 
 fun set_counterexample counterexample (Result r) =
@@ -153,7 +150,7 @@
   Unsynchronized.change result_ref (cons_report size report)
 
 fun add_response names eval_terms response result_ref =
-  Unsynchronized.change result_ref (set_reponse names eval_terms response)
+  Unsynchronized.change result_ref (set_response names eval_terms response)
 
 (* expectation *)
 
@@ -275,18 +272,6 @@
 type compile_generator =
   Proof.context -> (term * term list) list -> int list -> term list option * report option
 
-fun check_test_term t =
-  let
-    val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
-      error "Term to be tested contains type variables";
-    val _ = null (Term.add_vars t []) orelse
-      error "Term to be tested contains schematic variables";
-  in () end
-
-fun cpu_time description e =
-  let val ({cpu, ...}, result) = Timing.timing e ()
-  in (result, (description, Time.toMilliseconds cpu)) end
-
 fun limit timeout (limit_time, is_interactive) f exc () =
   if limit_time then
       TimeLimit.timeLimit timeout f ()
@@ -295,205 +280,9 @@
   else
     f ()
 
-fun test_term compile ctxt (limit_time, is_interactive) (t, eval_terms) =
-  let
-    fun message s = if Config.get ctxt quiet then () else Output.urgent_message s
-    val _ = check_test_term t
-    val names = Term.add_free_names t []
-    val current_size = Unsynchronized.ref 0
-    val current_result = Unsynchronized.ref empty_result 
-    fun excipit () =
-      "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
-    fun with_size test_fun k =
-      if k > Config.get ctxt size then
-        NONE
-      else
-        let
-          val _ = message ("Test data size: " ^ string_of_int k)
-          val _ = current_size := k
-          val ((result, report), timing) =
-            cpu_time ("size " ^ string_of_int k) (fn () => test_fun [1, k - 1])
-          val _ = add_timing timing current_result
-          val _ = add_report k report current_result
-        in
-          case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q
-        end;
-  in
-    (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)(
-      let
-        val (test_fun, comp_time) = cpu_time "quickcheck compilation"
-          (fn () => compile ctxt [(t, eval_terms)]);
-        val _ = add_timing comp_time current_result
-        val (response, exec_time) =
-          cpu_time "quickcheck execution" (fn () => with_size test_fun 1)
-        val _ = add_response names eval_terms response current_result
-        val _ = add_timing exec_time current_result
-      in !current_result end)
-(*    (fn () => (message (excipit ()); !current_result)) ()*)
-  end;
-
-fun validate_terms ctxt ts =
-  let
-    val _ = map check_test_term ts
-    val size = Config.get ctxt size
-    val (test_funs, comp_time) = cpu_time "quickcheck batch compilation"
-      (fn () => mk_batch_validator ctxt ts) 
-    fun with_size tester k =
-      if k > size then true
-      else if tester k then with_size tester (k + 1) else false
-    val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
-        Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt timeout))
-              (fn () => with_size test_fun 1) ()
-             handle TimeLimit.TimeOut => true)) test_funs)
-  in
-    (results, [comp_time, exec_time])
-  end
-  
-fun test_terms ctxt ts =
-  let
-    val _ = map check_test_term ts
-    val size = Config.get ctxt size
-    val namess = map (fn t => Term.add_free_names t []) ts
-    val (test_funs, comp_time) =
-      cpu_time "quickcheck batch compilation" (fn () => mk_batch_tester ctxt ts) 
-    fun with_size tester k =
-      if k > size then NONE
-      else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1)
-    val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () =>
-        Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt timeout))
-              (fn () => with_size test_fun 1) ()
-             handle TimeLimit.TimeOut => NONE)) test_funs)
-  in
-    (Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results,
-      [comp_time, exec_time])
-  end
-
-(* FIXME: this function shows that many assumptions are made upon the generation *)
-(* In the end there is probably no generic quickcheck interface left... *)
-
-fun test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) ts =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    fun message s = if Config.get ctxt quiet then () else Output.urgent_message s
-    val (ts', eval_terms) = split_list ts
-    val _ = map check_test_term ts'
-    val names = Term.add_free_names (hd ts') []
-    val Ts = map snd (Term.add_frees (hd ts') [])
-    val current_result = Unsynchronized.ref empty_result
-    fun test_card_size test_fun (card, size) =
-      (* FIXME: why decrement size by one? *)
-      let
-        val (ts, timing) =
-          cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
-            (fn () => fst (test_fun [card, size - 1]))
-        val _ = add_timing timing current_result
-      in
-        Option.map (pair card) ts
-      end
-    val enumeration_card_size =
-      if forall (fn T => Sign.of_sort thy (T,  ["Enum.enum"])) Ts then
-        (* size does not matter *)
-        map (rpair 0) (1 upto (length ts))
-      else
-        (* size does matter *)
-        map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt size))
-        |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
-  in
-    (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)(
-      let
-        val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => compile ctxt ts)
-        val _ = add_timing comp_time current_result     
-        val _ = case get_first (test_card_size test_fun) enumeration_card_size of
-          SOME (card, ts) => add_response names (nth eval_terms (card - 1)) (SOME ts) current_result
-        | NONE => ()
-      in !current_result end)
-      (*(fn () => (message "Quickcheck ran out of time"; !current_result)) ()*)
-  end
-
-fun get_finite_types ctxt =
-  fst (chop (Config.get ctxt finite_type_size)
-    (map (Type o rpair []) ["Enum.finite_1", "Enum.finite_2", "Enum.finite_3",
-     "Enum.finite_4", "Enum.finite_5"]))
-
-exception WELLSORTED of string
-
-fun monomorphic_term thy insts default_T =
-  let
-    fun subst (T as TFree (v, S)) =
-      let
-        val T' = AList.lookup (op =) insts v
-          |> the_default default_T
-      in if Sign.of_sort thy (T', S) then T'
-        else raise (WELLSORTED ("For instantiation with default_type " ^
-          Syntax.string_of_typ_global thy default_T ^
-          ":\n" ^ Syntax.string_of_typ_global thy T' ^
-          " to be substituted for variable " ^
-          Syntax.string_of_typ_global thy T ^ " does not have sort " ^
-          Syntax.string_of_sort_global thy S))
-      end
-      | subst T = T;
-  in (map_types o map_atyps) subst end;
-
-datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list
-
-fun instantiate_goals lthy insts goals =
-  let
-    fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms)
-    val thy = Proof_Context.theory_of lthy
-    val default_insts =
-      if Config.get lthy finite_types then (get_finite_types lthy) else (default_type lthy)
-    val inst_goals =
-      map (fn (check_goal, eval_terms) =>
-        if not (null (Term.add_tfree_names check_goal [])) then
-          map (fn T =>
-            (pair (SOME T) o Term o apfst (Object_Logic.atomize_term thy))
-              (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms))
-              handle WELLSORTED s => (SOME T, Wellsorted_Error s)) default_insts
-        else
-          [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) goals
-    val error_msg =
-      cat_lines
-        (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
-    fun is_wellsorted_term (T, Term t) = SOME (T, t)
-      | is_wellsorted_term (_, Wellsorted_Error s) = NONE
-    val correct_inst_goals =
-      case map (map_filter is_wellsorted_term) inst_goals of
-        [[]] => error error_msg
-      | xs => xs
-    val _ = if Config.get lthy quiet then () else warning error_msg
-  in
-    correct_inst_goals
-  end
-
-fun collect_results f [] results = results
-  | collect_results f (t :: ts) results =
-    let
-      val result = f t
-    in
-      if found_counterexample result then
-        (result :: results)
-      else
-        collect_results f ts (result :: results)
-    end  
-
-fun generator_test_goal_terms compile ctxt (limit_time, is_interactive) insts goals =
-  let
-    fun test_term' goal =
-      case goal of
-        [(NONE, t)] => test_term compile ctxt (limit_time, is_interactive) t
-      | ts => test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) (map snd ts)
-    val correct_inst_goals = instantiate_goals ctxt insts goals
-  in
-    if Config.get ctxt finite_types then
-      collect_results test_term' correct_inst_goals []
-    else
-      collect_results (test_term compile ctxt (limit_time, is_interactive))
-        (maps (map snd) correct_inst_goals) []
-  end;
-
 fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s
   
-fun test_goal_terms ctxt (limit_time, is_interactive) insts goals =
+fun test_terms ctxt (limit_time, is_interactive) insts goals =
   case active_testers ctxt of
     [] => error "No active testers for quickcheck"
   | testers => limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
@@ -524,7 +313,7 @@
         map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
           (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
   in
-    test_goal_terms lthy (time_limit, is_interactive) insts goals
+    test_terms lthy (time_limit, is_interactive) insts goals
   end
 
 (* pretty printing *)
@@ -537,7 +326,7 @@
         map (fn (s, t) =>
           Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex))
         @ (if null eval_terms then []
-           else (Pretty.str ("Evaluated terms:\n") ::
+           else (Pretty.fbrk :: Pretty.str ("Evaluated terms:") ::
              map (fn (t, u) =>
                Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1,
                  Syntax.pretty_term ctxt u]) (rev eval_terms))));