merged
authorwenzelm
Fri, 03 Dec 2010 17:18:41 +0100
changeset 40935 f48c5b951042
parent 40934 178c6654568c (diff)
parent 40896 d9c112c587f9 (current diff)
child 40936 10aeae27c7a6
merged
--- a/Admin/isatest/isatest-lint	Fri Dec 03 17:16:53 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Florian Haftmann, TUM
-#
-# Do consistency and quality checks on the isabelle sources
-#
-
-use strict;
-use File::Find;
-use File::Basename;
-
-# configuration
-my $isabelleRoot = $ENV{'HOME'} . "/isabelle";
-my @suffices = ('\.thy', '\.ml', '\.ML');
-
-# lint main procedure
-sub lint() {
-    my ($basename, $dirname, $ext) = fileparse($File::Find::name, @suffices);
-    if ($ext) {
-        open ISTREAM, $File::Find::name or die("error opening $File::Find::name");
-        my $found = 0;
-        while (<ISTREAM>) {
-            $found ||= m/\$Id[^\$]*\$/;
-            last if $found;
-        }
-        close ISTREAM;
-        my $relname = substr($File::Find::name, (length $isabelleRoot) + 1);
-        if (! $found) {
-            print "Found no CVS id in $relname\n";
-        }
-    }
-}
-
-# first argument =^= isabelle repository root
-if (@ARGV) {
-    $isabelleRoot = $ARGV[0];
-}
-
-find(\&lint, $isabelleRoot);
-
--- a/NEWS	Fri Dec 03 17:16:53 2010 +0100
+++ b/NEWS	Fri Dec 03 17:18:41 2010 +0100
@@ -101,6 +101,14 @@
 
 *** HOL ***
 
+* Quickcheck now by default uses exhaustive testing instead of random testing.
+Random testing can be invoked by quickcheck[random],
+exhaustive testing by quickcheck[exhaustive].
+
+* Quickcheck instantiates polymorphic types with small finite datatypes
+by default. This enables a simple execution mechanism to handle
+quantifiers and function equality over the finite datatypes.   
+
 * Functions can be declared as coercions and type inference will add them
 as necessary upon input of a term. In Complex_Main, real :: nat => real
 and real :: int => real are declared as coercions. A new coercion function
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -929,14 +929,21 @@
     and \emph{code} for code generation in SML.
 
   \item @{command (HOL) "quickcheck"} tests the current goal for
-    counter examples using a series of arbitrary assignments for its
+    counter examples using a series of assignments for its
     free variables; by default the first subgoal is tested, an other
     can be selected explicitly using an optional goal index.
+    Assignments can be chosen exhausting the search space upto a given
+    size or using a fixed number of random assignments in the search space.
+    By default, quickcheck uses exhaustive testing.
     A number of configuration options are supported for
     @{command (HOL) "quickcheck"}, notably:
 
     \begin{description}
 
+    \item[@{text tester}] specifies how to explore the search space
+      (e.g. exhaustive or random).
+      An unknown configuration option is treated as an argument to tester,
+      making @{text "tester ="} optional.
     \item[@{text size}] specifies the maximum size of the search space
     for assignment values.
 
--- a/src/HOL/Enum.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Enum.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -46,14 +46,14 @@
 
 end
 
+lemma [code]:
+  "HOL.equal f g \<longleftrightarrow>  list_all (%x. f x = g x) enum"
+by (auto simp add: list_all_iff enum_all equal fun_eq_iff)
+
 lemma [code nbe]:
   "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
   by (fact equal_refl)
 
-lemma [code]:
-  "HOL.equal f g \<longleftrightarrow>  list_all (%x. f x = g x) enum"
-by (auto simp add: list_all_iff enum_all equal fun_eq_iff)
-
 lemma order_fun [code]:
   fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
   shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
@@ -318,6 +318,8 @@
 
 datatype finite_1 = a\<^isub>1
 
+notation (output) a\<^isub>1  ("a\<^isub>1")
+
 instantiation finite_1 :: enum
 begin
 
@@ -352,6 +354,9 @@
 
 datatype finite_2 = a\<^isub>1 | a\<^isub>2
 
+notation (output) a\<^isub>1  ("a\<^isub>1")
+notation (output) a\<^isub>2  ("a\<^isub>2")
+
 instantiation finite_2 :: enum
 begin
 
@@ -388,6 +393,10 @@
 
 datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
 
+notation (output) a\<^isub>1  ("a\<^isub>1")
+notation (output) a\<^isub>2  ("a\<^isub>2")
+notation (output) a\<^isub>3  ("a\<^isub>3")
+
 instantiation finite_3 :: enum
 begin
 
@@ -422,6 +431,11 @@
 
 datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
 
+notation (output) a\<^isub>1  ("a\<^isub>1")
+notation (output) a\<^isub>2  ("a\<^isub>2")
+notation (output) a\<^isub>3  ("a\<^isub>3")
+notation (output) a\<^isub>4  ("a\<^isub>4")
+
 instantiation finite_4 :: enum
 begin
 
@@ -438,6 +452,12 @@
 
 datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
 
+notation (output) a\<^isub>1  ("a\<^isub>1")
+notation (output) a\<^isub>2  ("a\<^isub>2")
+notation (output) a\<^isub>3  ("a\<^isub>3")
+notation (output) a\<^isub>4  ("a\<^isub>4")
+notation (output) a\<^isub>5  ("a\<^isub>5")
+
 instantiation finite_5 :: enum
 begin
 
--- a/src/HOL/Finite_Set.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -517,6 +517,9 @@
 lemma finite [simp]: "finite (A \<Colon> 'a set)"
   by (rule subset_UNIV finite_UNIV finite_subset)+
 
+lemma finite_code [code]: "finite (A \<Colon> 'a set) = True"
+  by simp
+
 end
 
 lemma UNIV_unit [no_atp]:
--- a/src/HOL/Library/SML_Quickcheck.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Library/SML_Quickcheck.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -7,7 +7,21 @@
 
 setup {*
   Inductive_Codegen.quickcheck_setup #>
-  Context.theory_map (Quickcheck.add_generator ("SML", Codegen.test_term))
+  Context.theory_map (Quickcheck.add_generator ("SML",
+    fn ctxt => fn t =>
+      let
+        val test_fun = Codegen.test_term ctxt t 
+        val iterations = Config.get ctxt Quickcheck.iterations
+        fun iterate size 0 = NONE
+          | iterate size j =
+            let
+              val result = test_fun size handle Match => 
+                (if Config.get ctxt Quickcheck.quiet then ()
+                 else warning "Exception Match raised during quickcheck"; NONE)
+            in
+              case result of NONE => iterate size (j - 1) | SOME q => SOME q
+            end
+     in fn size => (iterate size iterations, NONE) end))
 *}
 
 end
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -231,7 +231,7 @@
       with wf less loc
       have "approx_stk G hp [xcp] ST'"
         by (auto simp add: sup_state_conv approx_stk_def approx_val_def 
-                 elim: conf_widen split: Err.split)
+                 elim: conf_widen split: err.split)
       moreover
       note len pc
       ultimately
@@ -702,7 +702,7 @@
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 split_beta split: option.split List.split split_if_asm)
+apply (clarsimp simp add: defs2 split_beta split: option.split list.split split_if_asm)
 apply (frule conf_widen)
 prefer 2
   apply assumption
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -17,13 +17,24 @@
 fun run_atp force_full_types timeout i n ctxt goal name =
   let
     val thy = ProofContext.theory_of ctxt
-    val params as {full_types, ...} =
+    val chained_ths = [] (* a tactic has no chained ths *)
+    val params as {full_types, relevance_thresholds, max_relevant, ...} =
       ((if force_full_types then [("full_types", "true")] else [])
-       @ [("timeout", Int.toString (Time.toMilliseconds timeout) ^ " ms")])
-(*      @ [("overlord", "true")] *)
+       @ [("timeout", Int.toString (Time.toSeconds timeout))])
+       @ [("overlord", "true")]
       |> Sledgehammer_Isar.default_params ctxt
     val prover = Sledgehammer.get_prover thy false name
-    val facts = []
+    val default_max_relevant =
+      Sledgehammer.default_max_relevant_for_prover thy name
+    val is_built_in_const =
+      Sledgehammer.is_built_in_const_for_prover ctxt name
+    val relevance_fudge = Sledgehammer.relevance_fudge_for_prover name
+    val relevance_override = {add = [], del = [], only = false}
+    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
+    val facts =
+      Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds
+          (the_default default_max_relevant max_relevant) is_built_in_const
+          relevance_fudge relevance_override chained_ths hyp_ts concl_t
     (* Check for constants other than the built-in HOL constants. If none of
        them appear (as should be the case for TPTP problems, unless "auto" or
        "simp" already did its "magic"), we can skip the relevance filter. *)
@@ -32,11 +43,14 @@
                                       not (String.isSubstring "HOL" s))
                         (prop_of goal))
     val problem =
-      {state = Proof.init ctxt, goal = goal, subgoal = i, facts = [],
+      {state = Proof.init ctxt, goal = goal, subgoal = i,
+       facts = map Sledgehammer.Untranslated facts,
        only = true, subgoal_count = n}
   in
-    prover params (K "") problem |> #message
-    handle ERROR message => "Error: " ^ message ^ "\n"
+    (case prover params (K "") problem of
+      {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
+    | _ => NONE)
+      handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
   end
 
 fun to_period ("." :: _) = []
@@ -44,12 +58,6 @@
   | to_period (s :: ss) = s :: to_period ss
   | to_period [] = []
 
-val extract_metis_facts =
-  space_explode " "
-  #> fold (maps o space_explode) ["(", ")", Symbol.ENQ, Symbol.ACK, "\n"]
-  #> fst o chop_while (not o member (op =) ["metis", "metisFT"])
-  #> (fn _ :: ss => SOME (to_period ss) | _ => NONE)
-
 val atp = "e" (* or "vampire" *)
 
 fun thms_of_name ctxt name =
@@ -68,19 +76,20 @@
 fun sledgehammer_with_metis_tac ctxt i th =
   let
     val thy = ProofContext.theory_of ctxt
-    val timeout = Time.fromSeconds (60 * 60 * 24 * 365) (* one year *)
-    val s = run_atp false timeout i i ctxt th atp
-    val xs = these (extract_metis_facts s)
-    val ths = maps (thms_of_name ctxt) xs
-  in Metis_Tactics.metis_tac ctxt ths i th end
+    val timeout = Time.fromSeconds 30
+  in
+    case run_atp false timeout i i ctxt th atp of
+      SOME facts => Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
+    | NONE => Seq.empty
+  end
 
 fun sledgehammer_as_oracle_tac ctxt i th =
   let
     val thy = ProofContext.theory_of ctxt
-    val timeout = Time.fromSeconds (60 * 60 * 24 * 365) (* one year *)
-    val s = run_atp true timeout i i ctxt th atp
+    val timeout = Time.fromSeconds 30
+    val xs = run_atp true timeout i i ctxt th atp
   in
-    if is_some (extract_metis_facts s) then Skip_Proof.cheat_tac thy th
+    if is_some xs then Skip_Proof.cheat_tac thy th
     else Seq.empty
   end
 
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -313,7 +313,7 @@
 
 lemma snd_linear: "linear snd" unfolding linear_def by (simp add: algebra_simps)
 
-lemma fst_snd_linear: "linear (%z. fst z + snd z)" unfolding linear_def by (simp add: algebra_simps)
+lemma fst_snd_linear: "linear (%(x,y). x + y)" unfolding linear_def by (simp add: algebra_simps)
 
 lemma scaleR_2:
   fixes x :: "'a::real_vector"
@@ -5451,11 +5451,11 @@
 shows "convex hull (S \<oplus> T) = (convex hull S) \<oplus> (convex hull T)"
 proof-
 have "(convex hull S) \<oplus> (convex hull T) =
-      (%z. fst z + snd z) ` ((convex hull S) <*> (convex hull T))"
+      (%(x,y). x + y) ` ((convex hull S) <*> (convex hull T))"
    by (simp add: set_plus_image)
-also have "... = (%z. fst z + snd z) ` (convex hull (S <*> T))" using convex_hull_direct_sum by auto
+also have "... = (%(x,y). x + y) ` (convex hull (S <*> T))" using convex_hull_direct_sum by auto
 also have "...= convex hull (S \<oplus> T)" using fst_snd_linear linear_conv_bounded_linear
-   convex_hull_linear_image[of "(%z. fst z + snd z)" "S <*> T"] by (auto simp add: set_plus_image)
+   convex_hull_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image)
 finally show ?thesis by auto
 qed
 
@@ -5464,11 +5464,11 @@
 assumes "convex S" "convex T"
 shows "rel_interior (S \<oplus> T) = (rel_interior S) \<oplus> (rel_interior T)"
 proof-
-have "(rel_interior S) \<oplus> (rel_interior T) = (%z. fst z + snd z) ` (rel_interior S <*> rel_interior T)"
+have "(rel_interior S) \<oplus> (rel_interior T) = (%(x,y). x + y) ` (rel_interior S <*> rel_interior T)"
    by (simp add: set_plus_image)
-also have "... = (%z. fst z + snd z) ` rel_interior (S <*> T)" using rel_interior_direct_sum assms by auto
+also have "... = (%(x,y). x + y) ` rel_interior (S <*> T)" using rel_interior_direct_sum assms by auto
 also have "...= rel_interior (S \<oplus> T)" using fst_snd_linear convex_direct_sum assms
-   rel_interior_convex_linear_image[of "(%z. fst z + snd z)" "S <*> T"] by (auto simp add: set_plus_image)
+   rel_interior_convex_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image)
 finally show ?thesis by auto
 qed
 
--- a/src/HOL/Mutabelle/MutabelleExtra.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -26,7 +26,7 @@
 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 {* Auto_Tools.time_limit := 10.0 *}
 
 ML {* val mtds = [
   MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
--- a/src/HOL/Mutabelle/mutabelle.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Fri Dec 03 17:18:41 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
@@ -497,9 +497,12 @@
  (map_types (inst_type insts) (freeze t));
 
 fun is_executable thy insts th =
-  ((Quickcheck.test_term
-      ((Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) (ProofContext.init_global thy))
-      (SOME (!testgen_name)) (preprocess thy insts (prop_of th));
+  ((Quickcheck.test_term 
+      (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))
-       (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);
 
 
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -114,13 +114,14 @@
 (** quickcheck **)
 
 fun invoke_quickcheck change_options quickcheck_generator thy t =
-  TimeLimit.timeLimit (Time.fromSeconds (!Auto_Tools.time_limit))
+  TimeLimit.timeLimit (seconds (!Auto_Tools.time_limit))
       (fn _ =>
           case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
-              (SOME quickcheck_generator, []) [t] of
+              false [] [t] of
             (NONE, _) => (NoCex, ([], NONE))
           | (SOME _, _) => (GenuineCex, ([], NONE))) ()
-  handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Tools.time_limit)], NONE))
+  handle TimeLimit.TimeOut =>
+         (Timeout, ([("timelimit", Real.floor (!Auto_Tools.time_limit))], NONE))
 
 fun quickcheck_mtd change_options quickcheck_generator =
   ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)
@@ -331,7 +332,7 @@
       (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)))
+        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)
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -33,7 +33,7 @@
 
 lemma
   "w \<in> S\<^isub>1 \<Longrightarrow> w = []"
-quickcheck[generator = prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1, expect = counterexample]
 oops
 
 definition "filter_a = filter (\<lambda>x. x = a)"
@@ -67,7 +67,7 @@
 
 theorem S\<^isub>1_sound:
 "w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator = prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1, expect = counterexample]
 oops
 
 
@@ -91,7 +91,7 @@
 
 theorem S\<^isub>2_sound:
 "w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1, expect = counterexample]
 oops
 
 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
@@ -113,7 +113,7 @@
 
 lemma S\<^isub>3_sound:
 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=prolog, iterations=1, size=1, expect = no_counterexample]
+quickcheck[tester = prolog, iterations=1, size=1, expect = no_counterexample]
 oops
 
 
@@ -131,7 +131,7 @@
 
 theorem S\<^isub>3_complete:
 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
-quickcheck[generator = prolog, size=1, iterations=1]
+quickcheck[tester = prolog, size=1, iterations=1]
 oops
 *)
 
@@ -156,7 +156,7 @@
 
 theorem S\<^isub>4_sound:
 "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator = prolog, size=1, iterations=1, expect = no_counterexample]
+quickcheck[tester = prolog, size=1, iterations=1, expect = no_counterexample]
 oops
 
 (*
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -23,8 +23,8 @@
 setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
 
 lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
-quickcheck[generator = code, iterations = 10000, report]
-quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = random, iterations = 10000, report]
+quickcheck[tester = prolog, iterations = 1, expect = counterexample]
 oops
 
 section {* Manual setup to find the counterexample *}
@@ -39,7 +39,7 @@
 
 lemma
   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
 oops
 
 setup {* Code_Prolog.map_code_options (K 
@@ -52,7 +52,7 @@
 
 lemma
   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = counterexample]
 oops
 
 section {* Simulating a global depth limit manually by limiting all predicates *}
@@ -70,7 +70,7 @@
 
 lemma
   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
 oops
 
 setup {*
@@ -86,7 +86,7 @@
 
 lemma
   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = counterexample]
 oops
 
 section {* Using a global limit for limiting the execution *} 
@@ -105,7 +105,7 @@
 
 lemma
   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
 oops
 
 text {* But a global depth limit of 14 does. *}
@@ -122,7 +122,7 @@
 
 lemma
   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = counterexample]
 oops
 
 end
\ No newline at end of file
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -50,8 +50,8 @@
 
 lemma
   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample, timeout = 60]
-quickcheck[generator = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample, timeout = 60]
+quickcheck[tester = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample, timeout = 60]
+quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample, timeout = 60]
 oops
 
 
--- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -27,7 +27,7 @@
 
 lemma
   "exec c s s' ==> exec (Seq c c) s s'"
-quickcheck[generator = predicate_compile_wo_ff, size = 2, iterations = 10, expect = counterexample]
+quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10, expect = counterexample]
 oops
 
 
--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -30,7 +30,7 @@
 
 lemma
   "exec c s s' ==> exec (Seq c c) s s'"
-quickcheck[generator = predicate_compile_wo_ff, size = 2, iterations = 10]
+quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10]
 oops
 
 
--- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -30,7 +30,7 @@
 
 lemma
   "exec c s s' ==> exec (Seq c c) s s'"
-  quickcheck[generator = predicate_compile_ff_nofs, size=2, iterations=10, quiet = false, expect = counterexample]
+  quickcheck[tester = predicate_compile_ff_nofs, size=2, iterations=10, quiet = false, expect = counterexample]
 oops
 
 
--- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -31,7 +31,7 @@
 lemma
   "exec c s s' ==> exec (Seq c c) s s'"
   nitpick (* nitpick fails here! *)
-  quickcheck[generator = predicate_compile_wo_ff, size=2, iterations=10, expect=counterexample]
+  quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=10, expect=counterexample]
 oops
 
 end
\ No newline at end of file
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -92,7 +92,7 @@
 
 lemma
   "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
-quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = counterexample]
 oops
 
 text {* Verifying that the found counterexample really is one by means of a proof *}
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -16,9 +16,9 @@
    manual_reorder = []}) *}
 
 lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
-quickcheck[generator = code, iterations = 10000]
-quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
-quickcheck[generator = prolog, expect = counterexample]
+quickcheck[tester = random, iterations = 10000]
+quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, expect = counterexample]
 oops
 
 end
\ No newline at end of file
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -48,7 +48,7 @@
 
 lemma
   "is_ten x = is_eleven x"
-quickcheck[generator = predicate_compile_wo_ff, iterations = 1, size = 1, expect = counterexample]
+quickcheck[tester = predicate_compile_wo_ff, iterations = 1, size = 1, expect = counterexample]
 oops
 
 section {* Context Free Grammar *}
@@ -65,7 +65,7 @@
 
 lemma
   "w \<in> S\<^isub>1 \<Longrightarrow> w = []"
-quickcheck[generator = predicate_compile_ff_nofs, iterations=1]
+quickcheck[tester = predicate_compile_ff_nofs, iterations=1]
 oops
 
 theorem S\<^isub>1_sound:
@@ -136,7 +136,7 @@
 oops
 
 lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"
-quickcheck[size=10, generator = predicate_compile_ff_fs]
+quickcheck[size=10, tester = predicate_compile_ff_fs]
 oops
 
 theorem S\<^isub>3_complete:
@@ -157,12 +157,12 @@
 
 theorem S\<^isub>4_sound:
 "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1]
+quickcheck[tester = predicate_compile_ff_nofs, size=5, iterations=1]
 oops
 
 theorem S\<^isub>4_complete:
 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
-quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1]
+quickcheck[tester = predicate_compile_ff_nofs, size=5, iterations=1]
 oops
 
 hide_const a b
@@ -202,7 +202,7 @@
 
 lemma
   "exec c s s' ==> exec (Seq c c) s s'"
-  quickcheck[generator = predicate_compile_wo_ff, size=2, iterations=20, expect = counterexample]
+  quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=20, expect = counterexample]
 oops
 
 subsection {* Lambda *}
@@ -257,7 +257,7 @@
 
 lemma
   "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
-quickcheck[generator = predicate_compile_ff_fs, size = 7, iterations = 10]
+quickcheck[tester = predicate_compile_ff_fs, size = 7, iterations = 10]
 oops
 
 subsection {* JAD *}
@@ -341,12 +341,12 @@
   "jad_mv v = inflate o split zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
 
 lemma "matrix (M::int list list) rs cs \<Longrightarrow> False"
-quickcheck[generator = predicate_compile_ff_nofs, size = 6]
+quickcheck[tester = predicate_compile_ff_nofs, size = 6]
 oops
 
 lemma
   "\<lbrakk> matrix M rs cs ; length v = cs \<rbrakk> \<Longrightarrow> jad_mv v (jad M) = mv M v"
-quickcheck[generator = predicate_compile_wo_ff]
+quickcheck[tester = predicate_compile_wo_ff]
 oops
 
 end
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -89,9 +89,9 @@
 
 lemma "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
 (*nitpick
-quickcheck[generator = code, iterations = 10000]
-quickcheck[generator = predicate_compile_wo_ff]
-quickcheck[generator = predicate_compile_ff_fs]
+quickcheck[tester = random, iterations = 10000]
+quickcheck[tester = predicate_compile_wo_ff]
+quickcheck[tester = predicate_compile_ff_fs]
 oops*)
 oops
 
@@ -115,10 +115,10 @@
  prolog-style generation. *}
 
 lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
-quickcheck[generator = code, iterations = 100000, expect = counterexample]
-(*quickcheck[generator = predicate_compile_wo_ff]*)
-(*quickcheck[generator = predicate_compile_ff_fs, iterations = 1]*)
-(*quickcheck[generator = prolog, iterations = 1, size = 1]*)
+quickcheck[tester = random, iterations = 100000, expect = counterexample]
+(*quickcheck[tester = predicate_compile_wo_ff]*)
+(*quickcheck[tester = predicate_compile_ff_fs, iterations = 1]*)
+(*quickcheck[tester = prolog, iterations = 1, size = 1]*)
 oops
 
 section {* Given a partial solution *}
@@ -130,8 +130,8 @@
   assumes "q = Seq (Sym N0) (Sym N0)"
 (*  assumes "s = [N0, N0]"*)
   shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
-(*quickcheck[generator = predicate_compile_wo_ff, iterations = 1]*)
-quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample]
+(*quickcheck[tester = predicate_compile_wo_ff, iterations = 1]*)
+quickcheck[tester = prolog, iterations = 1, size = 1, expect = counterexample]
 oops
 
 section {* Checking the counterexample *}
@@ -147,7 +147,7 @@
   assumes "q = Seq (Sym N0) (Sym N0)"
   assumes "s = [N0, N0]"
   shows "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
-(*quickcheck[generator = predicate_compile_wo_ff]*)
+(*quickcheck[tester = predicate_compile_wo_ff]*)
 oops
 
 lemma
@@ -157,8 +157,8 @@
   assumes "q = Seq (Sym N0) (Sym N0)"
   assumes "s = [N0, N0]"
   shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
-(*quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*)
-quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample]
+(*quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*)
+quickcheck[tester = prolog, iterations = 1, size = 1, expect = counterexample]
 oops
 
 lemma
@@ -168,13 +168,13 @@
   assumes "q = Seq (Sym N0) (Sym N0)"
   assumes "s = [N0, N0]"
 shows "prop_regex (n, (k, (p, (q, s))))"
-quickcheck[generator = predicate_compile_wo_ff]
-quickcheck[generator = prolog, expect = counterexample]
+quickcheck[tester = predicate_compile_wo_ff]
+quickcheck[tester = prolog, expect = counterexample]
 oops
 
 lemma "prop_regex a_sol"
-quickcheck[generator = code, expect = counterexample]
-quickcheck[generator = predicate_compile_ff_fs]
+quickcheck[tester = random, expect = counterexample]
+quickcheck[tester = predicate_compile_ff_fs]
 oops
 
 value [code] "prop_regex a_sol"
--- a/src/HOL/Product_Type.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Product_Type.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -160,7 +160,7 @@
 
 declare prod.simps(2) [nitpick_simp del]
 
-declare weak_case_cong [cong del]
+declare prod.weak_case_cong [cong del]
 
 
 subsubsection {* Tuple syntax *}
@@ -440,7 +440,7 @@
 
 lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
   -- {* Prevents simplification of @{term c}: much faster *}
-  by (fact weak_case_cong)
+  by (fact prod.weak_case_cong)
 
 lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
   by (simp add: split_eta)
@@ -578,7 +578,7 @@
   \medskip @{term split} used as a logical connective or set former.
 
   \medskip These rules are for use with @{text blast}; could instead
-  call @{text simp} using @{thm [source] split} as rewrite. *}
+  call @{text simp} using @{thm [source] prod.split} as rewrite. *}
 
 lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> split c p"
   apply (simp only: split_tupled_all)
--- a/src/HOL/Quickcheck.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Quickcheck.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -129,6 +129,7 @@
 use "Tools/quickcheck_generators.ML"
 setup Quickcheck_Generators.setup
 
+declare [[quickcheck_tester = random]]
 
 subsection {* Code setup *}
 
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -275,7 +275,7 @@
 proof (cases x, clarify)
   fix a b
   show "P (a, b)"
-  proof (induct a arbitrary: b rule: Nat.induct)
+  proof (induct a arbitrary: b rule: nat.induct)
     case zero
     show "P (0, b)" using assms by (induct b) auto
   next
--- a/src/HOL/Relation.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Relation.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -132,6 +132,11 @@
 lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)"
 by blast
 
+lemma Id_on_def'[nitpick_def, code]:
+  "(Id_on (A :: 'a => bool)) = (%(x, y). x = y \<and> A x)"
+by (auto simp add: fun_eq_iff
+  elim: Id_onE[unfolded mem_def] intro: Id_onI[unfolded mem_def])
+
 lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A"
 by blast
 
--- a/src/HOL/Smallcheck.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Smallcheck.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -48,7 +48,7 @@
 
 end
 
-section {* full small value generator type classes *}
+subsection {* full small value generator type classes *}
 
 class full_small = term_of +
 fixes full_small :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
@@ -80,7 +80,7 @@
 
 instantiation prod :: (full_small, full_small) full_small
 begin
-ML {* @{const_name "Pair"} *}
+
 definition
   "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
     %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d"
@@ -97,14 +97,16 @@
   "full_small_fun' f i d = (if i > 1 then
     full_small (%(a, at). full_small (%(b, bt).
       full_small_fun' (%(g, gt). f (g(a := b),
-        (%_. let T1 = (Typerep.typerep (TYPE('a))); T2 = (Typerep.typerep (TYPE('b))) in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
-         
-(Code_Evaluation.Const (STR ''Fun.fun_upd'')
-
-(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
-
- (gt ())) (at ())) (bt ())))) (i - 1) d) d) d else (if i > 0 then
-  full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
+        (%_. let T1 = (Typerep.typerep (TYPE('a)));
+                 T2 = (Typerep.typerep (TYPE('b)))
+             in
+               Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
+                 (Code_Evaluation.Const (STR ''Fun.fun_upd'')
+                    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
+                       Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
+               (gt ())) (at ())) (bt ())))) (i - 1) d) d) d
+  else (if i > 0 then
+    full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
 
 definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
 where
@@ -117,6 +119,11 @@
 
 subsection {* Defining combinators for any first-order data type *}
 
+definition orelse :: "'a option => 'a option => 'a option"
+where
+  [code_unfold]: "orelse x y = (case x of Some x' => Some x' | None => y)"
+
+
 definition catch_match :: "term list option => term list option => term list option"
 where
   [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
@@ -126,11 +133,11 @@
 
 use "Tools/smallvalue_generators.ML"
 
-(* We do not activate smallcheck yet.
 setup {* Smallvalue_Generators.setup *}
-*)
+
+declare [[quickcheck_tester = exhaustive]]
 
-hide_fact catch_match_def
-hide_const (open) catch_match
+hide_fact orelse_def catch_match_def
+hide_const (open) orelse catch_match
 
 end
\ No newline at end of file
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -628,9 +628,9 @@
 
     val ([dt_induct'], thy7) =
       thy6
-      |> Sign.add_path big_name
-      |> Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])]
-      ||> Sign.parent_path
+      |> Global_Theory.add_thms
+        [((Binding.qualify true big_name (Binding.name "induct"), dt_induct),
+          [case_names_induct])]
       ||> Theory.checkpoint;
 
   in
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -98,18 +98,18 @@
 
 fun store_thmss_atts label tnames attss thmss =
   fold_map (fn ((tname, atts), thms) =>
-    Sign.add_path tname
-    #> Global_Theory.add_thmss [((Binding.name label, thms), atts)]
-    #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
+    Global_Theory.add_thmss
+      [((Binding.qualify true tname (Binding.name label), thms), atts)]
+    #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
   ##> Theory.checkpoint;
 
 fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
 
 fun store_thms_atts label tnames attss thmss =
   fold_map (fn ((tname, atts), thms) =>
-    Sign.add_path tname
-    #> Global_Theory.add_thms [((Binding.name label, thms), atts)]
-    #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
+    Global_Theory.add_thms
+      [((Binding.qualify true tname (Binding.name label), thms), atts)]
+    #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
   ##> Theory.checkpoint;
 
 fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -362,14 +362,14 @@
   let
     val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
     val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
+    val prfx = Binding.qualify true (space_implode "_" new_type_names);
     val (((inject, distinct), [induct]), thy2) =
       thy1
       |> store_thmss "inject" new_type_names raw_inject
       ||>> store_thmss "distinct" new_type_names raw_distinct
-      ||> Sign.add_path (space_implode "_" new_type_names)
       ||>> Global_Theory.add_thms
-        [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])]
-      ||> Sign.restore_naming thy1;
+        [((prfx (Binding.name "induct"), raw_induct),
+          [mk_case_names_induct descr])];
   in
     thy2
     |> derive_datatype_props config dt_names alt_names [descr] sorts
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -383,9 +383,8 @@
             "set and display the default parameters for Nitpick"
             Keyword.thy_decl parse_nitpick_params_command
 
-fun auto_nitpick state =
-  if not (!auto) then (false, state) else pick_nits [] true 1 0 state
+val auto_nitpick = pick_nits [] true 1 0
 
-val setup = Auto_Tools.register_tool ("nitpick", auto_nitpick)
+val setup = Auto_Tools.register_tool (auto, auto_nitpick)
 
 end;
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -38,7 +38,7 @@
   val write_program : logic_program -> string
   val run : (Time.time * prolog_system) -> logic_program -> (string * prol_term list) -> string list -> int option -> prol_term list list
   
-  val quickcheck : Proof.context -> term -> int -> term list option * (bool list * bool)
+  val quickcheck : Proof.context -> term -> int -> term list option * Quickcheck.report option
 
   val trace : bool Unsynchronized.ref
   
@@ -129,8 +129,8 @@
 
 (* general string functions *)
 
-val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
-val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
+val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
+val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode;
 
 (* internal program representation *)
 
@@ -835,7 +835,7 @@
 
 val parse_term = fst o Scan.finite Symbol.stopper
     (Scan.error (!! (fn _ => raise Fail "parsing prolog output failed")) scan_term)
-  o explode
+  o raw_explode
   
 fun parse_solutions sol =
   let
@@ -1030,9 +1030,8 @@
       case tss of
         [ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ map snd vs'))
       | _ => NONE
-    val empty_report = ([], false)
   in
-    (res, empty_report)
+    (res, NONE)
   end; 
 
 end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -22,7 +22,7 @@
   val tracing : bool Unsynchronized.ref;
   val quiet : bool Unsynchronized.ref;
   val quickcheck_compile_term : Predicate_Compile_Aux.compilation -> bool -> bool -> int ->
-    Proof.context -> term -> int -> term list option * (bool list * bool);
+    Proof.context -> term -> int -> term list option * Quickcheck.report option;
 (*  val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
   val nrandom : int Unsynchronized.ref;
   val debug : bool Unsynchronized.ref;
@@ -344,9 +344,8 @@
 fun compile_term' compilation options depth ctxt t =
   let
     val c = compile_term compilation options ctxt t
-    val dummy_report = ([], false)
   in
-    fn size => (try_upto (!quiet) (c size (!nrandom)) depth, dummy_report)
+    fn size => (try_upto (!quiet) (c size (!nrandom)) depth, NONE)
   end
 
 fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -347,14 +347,11 @@
       parse_sledgehammer_params_command
 
 fun auto_sledgehammer state =
-  if not (!auto) then
-    (false, state)
-  else
-    let val ctxt = Proof.context_of state in
-      run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
-                       (minimize_command [] 1) state
-    end
+  let val ctxt = Proof.context_of state in
+    run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
+                     (minimize_command [] 1) state
+  end
 
-val setup = Auto_Tools.register_tool (sledgehammerN, auto_sledgehammer)
+val setup = Auto_Tools.register_tool (auto, auto_sledgehammer)
 
 end;
--- a/src/HOL/Tools/inductive.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/inductive.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -596,7 +596,7 @@
 
 val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop;
 val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop;
-    
+
 (* prove induction rule *)
 
 fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono
--- a/src/HOL/Tools/inductive_codegen.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -9,7 +9,7 @@
   val add : string option -> int option -> attribute
   val test_fn : (int * int * int -> term list option) Unsynchronized.ref
   val test_term:
-    Proof.context -> term -> int -> term list option * (bool list * bool)
+    Proof.context -> term -> int -> term list option * Quickcheck.report option
   val setup : theory -> theory
   val quickcheck_setup : theory -> theory
 end;
@@ -842,10 +842,9 @@
     val start = Config.get ctxt depth_start;
     val offset = Config.get ctxt size_offset;
     val test_fn' = !test_fn;
-    val dummy_report = ([], false)
     fun test k = (deepen bound (fn i =>
       (Output.urgent_message ("Search depth: " ^ string_of_int i);
-       test_fn' (i, values, k+offset))) start, dummy_report);
+       test_fn' (i, values, k+offset))) start, NONE);
   in test end;
 
 val quickcheck_setup =
--- a/src/HOL/Tools/quickcheck_generators.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -17,7 +17,7 @@
       string list * string list -> typ list * typ list -> theory -> theory)
     -> Datatype.config -> string list -> theory -> theory
   val compile_generator_expr:
-    Proof.context -> term -> int -> term list option * (bool list * bool)
+    Proof.context -> term -> int -> term list option * Quickcheck.report option
   val put_counterexample: (unit -> int -> seed -> term list option * seed)
     -> Proof.context -> Proof.context
   val put_counterexample_report: (unit -> int -> seed -> (term list option * (bool list * bool)) * seed)
@@ -387,25 +387,73 @@
     Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check))
   end
 
+(* single quickcheck report *)
+
+datatype single_report = Run of bool list * bool | MatchExc
+
+fun collect_single_report single_report
+    (Quickcheck.Report {iterations = iterations, raised_match_errors = raised_match_errors,
+    satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
+  case single_report
+  of MatchExc =>
+    Quickcheck.Report {iterations = iterations + 1, raised_match_errors = raised_match_errors + 1,
+      satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}
+   | Run (assms, concl) =>
+    Quickcheck.Report {iterations = iterations + 1, raised_match_errors = raised_match_errors,
+      satisfied_assms =
+        map2 (fn b => fn s => if b then s + 1 else s) assms
+         (if null satisfied_assms then replicate (length assms) 0 else satisfied_assms),
+      positive_concl_tests = if concl then positive_concl_tests + 1 else positive_concl_tests}
+
+val empty_report = Quickcheck.Report { iterations = 0, raised_match_errors = 0,
+  satisfied_assms = [], positive_concl_tests = 0 }
+    
 fun compile_generator_expr ctxt t =
   let
     val Ts = (map snd o fst o strip_abs) t;
     val thy = ProofContext.theory_of ctxt
-  in if Config.get ctxt Quickcheck.report then
-    let
-      val t' = mk_reporting_generator_expr thy t Ts;
-      val compile = Code_Runtime.dynamic_value_strict
-        (Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
-        thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t' [];
-    in compile #> Random_Engine.run end
-  else
-    let
-      val t' = mk_generator_expr thy t Ts;
-      val compile = Code_Runtime.dynamic_value_strict
-        (Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
-        thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t' [];
-      val dummy_report = ([], false)
-    in compile #> Random_Engine.run #> rpair dummy_report end
+    val iterations = Config.get ctxt Quickcheck.iterations
+  in
+    if Config.get ctxt Quickcheck.report then
+      let
+        val t' = mk_reporting_generator_expr thy t Ts;
+        val compile = Code_Runtime.dynamic_value_strict
+          (Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
+          thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t' [];
+        val single_tester = compile #> Random_Engine.run
+        fun iterate_and_collect size 0 report = (NONE, report)
+          | iterate_and_collect size j report =
+            let
+              val (test_result, single_report) = apsnd Run (single_tester size) handle Match => 
+                (if Config.get ctxt Quickcheck.quiet then ()
+                 else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
+              val report = collect_single_report single_report report
+            in
+              case test_result of NONE => iterate_and_collect size (j - 1) report
+                | SOME q => (SOME q, report)
+            end
+      in
+        fn size => apsnd SOME (iterate_and_collect size iterations empty_report)
+      end
+    else
+      let
+        val t' = mk_generator_expr thy t Ts;
+        val compile = Code_Runtime.dynamic_value_strict
+          (Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
+          thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t' [];
+        val single_tester = compile #> Random_Engine.run
+        fun iterate size 0 = NONE
+          | iterate size j =
+            let
+              val result = single_tester size handle Match => 
+                (if Config.get ctxt Quickcheck.quiet then ()
+                 else warning "Exception Match raised during quickcheck"; NONE)
+            in
+              case result of NONE => iterate size (j - 1) | SOME q => SOME q
+            end
+      in
+        fn size => (rpair NONE (iterate size iterations))
+      end
   end;
 
 
--- a/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -7,15 +7,25 @@
 signature SMALLVALUE_GENERATORS =
 sig
   val compile_generator_expr:
-    Proof.context -> term -> int -> term list option * (bool list * bool)
+    Proof.context -> term -> int -> term list option * Quickcheck.report option
   val put_counterexample: (unit -> int -> term list option)
     -> Proof.context -> Proof.context
+  val smart_quantifier : bool Config.T;
   val setup: theory -> theory
 end;
 
 structure Smallvalue_Generators : SMALLVALUE_GENERATORS =
 struct
 
+(* static options *)
+
+val define_foundationally = false
+
+(* dynamic options *)
+
+val (smart_quantifier, setup_smart_quantifier) =
+  Attrib.config_bool "quickcheck_smart_quantifier" (K true)
+
 (** general term functions **)
 
 fun mk_measure f =
@@ -36,6 +46,8 @@
   end
   | mk_sumcases _ f T = f T
 
+fun mk_undefined T = Const(@{const_name undefined}, T)
+  
 
 (** abstract syntax **)
 
@@ -50,8 +62,8 @@
   let
     val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
   in
-    Const (@{const_name Option.option_case}, T --> (T' --> T) --> T --> T)
-      $ y $ Const (@{const_name Some}, T' --> T) $ x
+    Const (@{const_name "Smallcheck.orelse"}, T --> T --> T)
+      $ x $ y
   end
 
 (** datatypes **)
@@ -70,11 +82,8 @@
 fun full_smallT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
   --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
  
-fun mk_equations thy descr vs tycos (names, auxnames) (Ts, Us) =
+fun mk_equations thy descr vs tycos smalls (Ts, Us) =
   let
-    val smallsN = map (prefix (full_smallN ^ "_")) (names @ auxnames);
-    val smalls = map2 (fn name => fn T => Free (name, full_smallT T))
-      smallsN (Ts @ Us)
     fun mk_small_call T =
       let
         val small = Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)        
@@ -119,44 +128,77 @@
     val lhss = map2 (fn t => fn T => t $ test_function T $ size) smalls (Ts @ Us);
     val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
   in
-    (Ts @ Us ~~ (smallsN ~~ eqs))
+    eqs
+  end
+
+(* foundational definition with the function package *)
+
+val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
+
+fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
+    Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
+
+fun mk_termination_measure T =
+  let
+    val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T))
+  in
+    mk_measure (mk_sumcases @{typ nat} mk_single_measure T')
   end
-    
-val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
-  
+
+fun termination_tac ctxt = 
+  Function_Relation.relation_tac ctxt mk_termination_measure 1
+  THEN rtac @{thm wf_measure} 1
+  THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac 
+    (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
+     @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
+
+fun pat_completeness_auto ctxt =
+  Pat_Completeness.pat_completeness_tac ctxt 1
+  THEN auto_tac (clasimpset_of ctxt)    
+
+
+(* creating the instances *)
+
 fun instantiate_smallvalue_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   let
     val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
-    val eqs = mk_equations thy descr vs tycos (names, auxnames) (Ts, Us)
-    fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
-      Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
-    fun mk_termination_measure T =
-      let
-        val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T))
-      in
-        mk_measure (mk_sumcases @{typ nat} mk_single_measure T')
-      end
-    fun termination_tac ctxt = 
-      Function_Relation.relation_tac ctxt mk_termination_measure 1
-      THEN rtac @{thm wf_measure} 1
-      THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac 
-        (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
-         @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
-    fun pat_completeness_auto ctxt =
-      Pat_Completeness.pat_completeness_tac ctxt 1
-      THEN auto_tac (clasimpset_of ctxt)
-  in 
+    val smallsN = map (prefix (full_smallN ^ "_")) (names @ auxnames);
+  in
     thy
     |> Class.instantiation (tycos, vs, @{sort full_small})
-    |> Function.add_function
-      (map (fn (T, (name, _)) =>
-          Syntax.no_syn (Binding.conceal (Binding.name name), SOME (full_smallT T))) eqs)
-        (map (pair (apfst Binding.conceal Attrib.empty_binding) o snd o snd) eqs)
-        Function_Common.default_config pat_completeness_auto
-    |> snd
-    |> Local_Theory.restore
-    |> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
-    |> snd
+    |> (if define_foundationally then
+      let
+        val smalls = map2 (fn name => fn T => Free (name, full_smallT T)) smallsN (Ts @ Us)
+        val eqs = mk_equations thy descr vs tycos smalls (Ts, Us)
+      in
+        Function.add_function
+          (map (fn (name, T) =>
+              Syntax.no_syn (Binding.conceal (Binding.name name), SOME (full_smallT T)))
+                (smallsN ~~ (Ts @ Us)))
+            (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs)
+          Function_Common.default_config pat_completeness_auto
+        #> snd
+        #> Local_Theory.restore
+        #> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
+        #> snd
+      end
+    else
+      fold_map (fn (name, T) => Local_Theory.define
+          ((Binding.conceal (Binding.name name), NoSyn),
+            (apfst Binding.conceal Attrib.empty_binding, mk_undefined (full_smallT T)))
+        #> apfst fst) (smallsN ~~ (Ts @ Us))
+      #> (fn (smalls, lthy) =>
+        let
+          val eqs_t = mk_equations thy descr vs tycos smalls (Ts, Us)
+          val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
+            (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
+        in
+          fold (fn (name, eq) => Local_Theory.note
+          ((Binding.conceal (Binding.qualify true prfx
+             (Binding.qualify true name (Binding.name "simps"))),
+             Code.add_default_eqn_attrib :: map (Attrib.internal o K)
+               [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (smallsN ~~ eqs) lthy
+        end))
     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   end handle FUNCTION_TYPE =>
     (Datatype_Aux.message config
@@ -173,12 +215,50 @@
 
 val target = "Quickcheck";
 
-fun mk_generator_expr thy prop Ts =
+fun mk_smart_generator_expr ctxt t =
   let
+    val ((vnames, Ts), t') = apfst split_list (strip_abs t)
+    val ([depth_name], ctxt') = Variable.variant_fixes ["depth"] ctxt
+    val (names, ctxt'') = Variable.variant_fixes vnames ctxt'
+    val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") vnames) ctxt''
+    val depth = Free (depth_name, @{typ code_numeral})
+    val frees = map2 (curry Free) names Ts
+    val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names 
+    fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
+      | strip_imp A = ([], A)
+    val (assms, concl) = strip_imp (subst_bounds (rev frees, t'))
+    val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
+    fun mk_small_closure (free as Free (_, T), term_var) t =
+      Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
+        $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
+          $ lambda free (lambda term_var t)) $ depth
+    fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
+    val none_t = @{term "None :: term list option"}
+    fun mk_safe_if (cond, then_t, else_t) =
+      @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $
+        (@{term "If :: bool => term list option => term list option => term list option"}
+        $ cond $ then_t $ else_t) $ none_t;
+    fun mk_test_term bound_vars assms =
+      let
+        fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
+        val (vars, check) =
+          case assms of [] =>
+            (vars_of concl, (concl, none_t, @{term "Some :: term list => term list option"} $ terms))
+          | assm :: assms =>
+            (vars_of assm, (assm, mk_test_term (union (op =) (vars_of assm) bound_vars) assms, none_t))
+      in
+        fold_rev mk_small_closure (map lookup vars) (mk_safe_if check)
+      end
+  in lambda depth (mk_test_term [] assms) end
+
+fun mk_generator_expr ctxt t =
+  let
+    val Ts = (map snd o fst o strip_abs) t;
+    val thy = ProofContext.theory_of ctxt
     val bound_max = length Ts - 1;
     val bounds = map_index (fn (i, ty) =>
       (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
-    val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
+    val result = list_comb (t, map (fn (i, _, _, _) => Bound i) bounds);
     val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
     val check =
       @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $
@@ -193,26 +273,22 @@
 
 fun compile_generator_expr ctxt t =
   let
-    val Ts = (map snd o fst o strip_abs) t;
     val thy = ProofContext.theory_of ctxt
-  in if Config.get ctxt Quickcheck.report then
-    error "Compilation with reporting facility is not supported"
-  else
-    let
-      val t' = mk_generator_expr thy t Ts;
-      val compile = Code_Runtime.dynamic_value_strict
-        (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
-        thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
-      val dummy_report = ([], false)
-    in compile #> rpair dummy_report end
-  end;
+    val t' =
+      (if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr)
+        ctxt t;
+    val compile = Code_Runtime.dynamic_value_strict
+      (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
+      thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
+  in fn size => rpair NONE (compile size) end;
 
 (** setup **)
 
 val setup =
   Datatype.interpretation
     (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype))
+  #> setup_smart_quantifier
   #> Context.theory_map
-    (Quickcheck.add_generator ("small", compile_generator_expr));
+    (Quickcheck.add_generator ("exhaustive", compile_generator_expr));
 
 end;
--- a/src/HOL/Tools/try.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/try.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -110,8 +110,8 @@
       (Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout)
                                     o Toplevel.proof_of)))
 
-fun auto_try st = if not (!auto) then (false, st) else do_try true NONE st
+val auto_try = do_try true NONE
 
-val setup = Auto_Tools.register_tool (tryN, auto_try)
+val setup = Auto_Tools.register_tool (auto, auto_try)
 
 end;
--- a/src/HOL/ex/Quickcheck_Examples.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -9,8 +9,6 @@
 imports Main
 begin
 
-setup {* Smallvalue_Generators.setup *}
-
 text {*
 The 'quickcheck' command allows to find counterexamples by evaluating
 formulae.
@@ -26,33 +24,33 @@
 subsection {* Lists *}
 
 theorem "map g (map f xs) = map (g o f) xs"
-  quickcheck[size = 3]
-  quickcheck[generator = random, expect = no_counterexample]
-  quickcheck[generator = small, size = 3, iterations = 1, report = false, expect = no_counterexample]
+  quickcheck[random, expect = no_counterexample]
+  quickcheck[exhaustive, size = 3, expect = no_counterexample]
   oops
 
 theorem "map g (map f xs) = map (f o g) xs"
-  quickcheck[generator = random, expect = counterexample]
-  quickcheck[generator = small, report = false]
+  quickcheck[random, expect = counterexample]
+  quickcheck[exhaustive, expect = counterexample]
   oops
 
 theorem "rev (xs @ ys) = rev ys @ rev xs"
-  quickcheck[expect = no_counterexample]
-  quickcheck[generator = small, expect = no_counterexample, report = false]
+  quickcheck[random, expect = no_counterexample]
+  quickcheck[exhaustive, expect = no_counterexample]
   oops
 
 theorem "rev (xs @ ys) = rev xs @ rev ys"
-  quickcheck[generator = small, expect = counterexample, report = false]
-  quickcheck[generator = random, expect = counterexample]
+  quickcheck[random, expect = counterexample]
+  quickcheck[exhaustive, expect = counterexample]
   oops
 
 theorem "rev (rev xs) = xs"
-  quickcheck[expect = no_counterexample]
+  quickcheck[random, expect = no_counterexample]
+  quickcheck[exhaustive, expect = no_counterexample]
   oops
 
 theorem "rev xs = xs"
-  quickcheck[generator = small, report = false]
-  quickcheck[expect = counterexample]
+  quickcheck[random, expect = counterexample]
+  quickcheck[exhaustive, expect = counterexample]
   oops
 
 text {* An example involving functions inside other data structures *}
@@ -62,13 +60,13 @@
   | "app (f # fs) x = app fs (f x)"
 
 lemma "app (fs @ gs) x = app gs (app fs x)"
-  quickcheck[generator = random, expect = no_counterexample]
-  quickcheck[generator = small, iterations = 1, size = 4, report = false, expect = no_counterexample]
+  quickcheck[random, expect = no_counterexample]
+  quickcheck[exhaustive, size = 4, expect = no_counterexample]
   by (induct fs arbitrary: x) simp_all
 
 lemma "app (fs @ gs) x = app fs (app gs x)"
-  quickcheck[generator = random, expect = counterexample]
-  quickcheck[generator = small, report = false, expect = counterexample]
+  quickcheck[random, expect = counterexample]
+  quickcheck[exhaustive, expect = counterexample]
   oops
 
 primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
@@ -82,19 +80,19 @@
 text {* A lemma, you'd think to be true from our experience with delAll *}
 lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
   -- {* Wrong. Precondition needed.*}
-  quickcheck[generator = small, report = false]
-  quickcheck[expect = counterexample]
+  quickcheck[random, expect = counterexample]
+  quickcheck[exhaustive, expect = counterexample]
   oops
 
 lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
-  quickcheck[generator = small, report = false]
-  quickcheck[expect = counterexample]
+  quickcheck[random, expect = counterexample]
+  quickcheck[exhaustive, expect = counterexample]
     -- {* Also wrong.*}
   oops
 
 lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
-  quickcheck[generator = small, report = false]
-  quickcheck[expect = no_counterexample]
+  quickcheck[random, expect = no_counterexample]
+  quickcheck[exhaustive, expect = no_counterexample]
   by (induct xs) auto
 
 primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
@@ -103,13 +101,14 @@
                             else (x#(replace a b xs)))"
 
 lemma "occurs a xs = occurs b (replace a b xs)"
-  quickcheck[generator = small, report = false]
-  quickcheck[expect = counterexample]
+  quickcheck[random, expect = counterexample]
+  quickcheck[exhaustive, expect = counterexample]
   -- {* Wrong. Precondition needed.*}
   oops
 
 lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
-  quickcheck[expect = no_counterexample, report = false]
+  quickcheck[random, expect = no_counterexample]
+  quickcheck[exhaustive, expect = no_counterexample]
   by (induct xs) simp_all
 
 
@@ -132,12 +131,14 @@
   | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
 
 theorem "plant (rev (leaves xt)) = mirror xt"
-  quickcheck[expect = counterexample]
+  quickcheck[random, expect = counterexample]
+  quickcheck[exhaustive, expect = counterexample]
     --{* Wrong! *} 
   oops
 
 theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
-  quickcheck[expect = counterexample]
+  quickcheck[random, expect = counterexample]
+  quickcheck[exhaustive, expect = counterexample]
     --{* Wrong! *} 
   oops
 
@@ -152,9 +153,9 @@
   | "root (Node f x y) = f"
 
 theorem "hd (inOrder xt) = root xt"
-  quickcheck[generator = small, report = false]
-  quickcheck[expect = counterexample]
-    --{* Wrong! *} 
+  quickcheck[random, expect = counterexample]
+  quickcheck[exhaustive, expect = counterexample]
+  --{* Wrong! *} 
   oops
 
 
@@ -165,75 +166,75 @@
 
 lemma
   "[] ~= xs ==> hd xs = last (x # xs)"
-quickcheck[generator = random, report = false]
-quickcheck[generator = small, report = false, expect = counterexample]
+quickcheck[random]
+quickcheck[exhaustive, expect = counterexample]
 oops
 
 lemma
   assumes "!!i. [| i < n; i < length xs |] ==> P (xs ! i)" "n < length xs ==> ~ P (xs ! n)"
   shows "drop n xs = takeWhile P xs"
-quickcheck[generator = random, iterations = 10000, report = false, quiet]
-quickcheck[generator = small, iterations = 1, report = false, expect = counterexample]
+quickcheck[random, iterations = 10000, quiet]
+quickcheck[exhaustive, expect = counterexample]
 oops
 
 lemma
   "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]"
-quickcheck[generator = random, iterations = 10000, report = false, quiet]
-quickcheck[generator = small, iterations = 1, report = false, expect = counterexample]
+quickcheck[random, iterations = 10000]
+quickcheck[exhaustive, expect = counterexample]
 oops
 
 lemma
   "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
-quickcheck[generator = random, iterations = 10000, report = false, quiet]
-quickcheck[generator = small, finite_types = false, report = false, expect = counterexample]
+quickcheck[random, iterations = 10000, finite_types = false]
+quickcheck[exhaustive, finite_types = false, expect = counterexample]
 oops
 
 lemma
   "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
-quickcheck[generator = random, iterations = 1000, report = false, quiet]
-quickcheck[generator = small, finite_types = false, report = false, expect = counterexample]
+quickcheck[random, iterations = 10000, finite_types = false]
+quickcheck[exhaustive, finite_types = false, expect = counterexample]
 oops
 
 lemma
   "ns ! k < length ns ==> k <= listsum ns"
-quickcheck[generator = random, iterations = 10000, report = true, quiet]
-quickcheck[generator = small, report = false, expect = counterexample]
+quickcheck[random, iterations = 10000, finite_types = false, quiet]
+quickcheck[exhaustive, finite_types = false, expect = counterexample]
 oops
 
 lemma
   "[| ys = x # xs1; zs = xs1 @ xs |] ==> ys @ zs = x # xs"
-quickcheck[generator = random, iterations = 10000, report = true]
-quickcheck[generator = small, report = false, expect = counterexample]
+quickcheck[random, iterations = 10000]
+quickcheck[exhaustive, expect = counterexample]
 oops
 
 lemma
 "i < length xs ==> take (Suc i) xs = [] @ xs ! i # take i xs"
-quickcheck[generator = random]
-quickcheck[generator = small, report = false, expect = counterexample]
+quickcheck[random, iterations = 10000]
+quickcheck[exhaustive, expect = counterexample]
 oops
 
 lemma
   "i < length xs ==> take (Suc i) xs = (xs ! i # xs) @ take i []"
-quickcheck[generator = random]
-quickcheck[generator = small, report = false, expect = counterexample]
+quickcheck[random, iterations = 10000]
+quickcheck[exhaustive, expect = counterexample]
 oops
 
 lemma
   "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]"
-quickcheck[generator = random]
-quickcheck[generator = small, report = false]
+quickcheck[random]
+quickcheck[exhaustive, expect = counterexample]
 oops
 
 lemma
   "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. {..<i} (length ys)]"
-quickcheck[generator = random]
-quickcheck[generator = small, report = false, expect = counterexample]
+quickcheck[random]
+quickcheck[exhaustive, expect = counterexample]
 oops
 
 lemma
   "(ys = zs) = (xs @ ys = splice xs zs)"
-quickcheck[generator = random]
-quickcheck[generator = small, report = false, expect = counterexample]
+quickcheck[random]
+quickcheck[exhaustive, expect = counterexample]
 oops
 
 section {* Examples with quantifiers *}
@@ -243,14 +244,17 @@
 *}
 
 lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
-  quickcheck[expect = counterexample]
+  quickcheck[random, expect = counterexample]
+  quickcheck[exhaustive, expect = counterexample]
 oops
 
 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
+  quickcheck[random, expect = counterexample]
   quickcheck[expect = counterexample]
 oops
 
 lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
+  quickcheck[random, expect = counterexample]
   quickcheck[expect = counterexample]
 oops
 
--- a/src/HOL/ex/set.thy	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/ex/set.thy	Fri Dec 03 17:18:41 2010 +0100
@@ -205,7 +205,7 @@
 lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
   P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
   -- {* Example 11: needs a hint. *}
-by(metis Nat.induct)
+by(metis nat.induct)
 
 lemma
   "(\<forall>A. (0, 0) \<in> A \<and> (\<forall>x y. (x, y) \<in> A \<longrightarrow> (Suc x, Suc y) \<in> A) \<longrightarrow> (n, m) \<in> A)
--- a/src/Pure/codegen.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/Pure/codegen.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -76,7 +76,7 @@
   val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
   val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
   val test_fn: (int -> term list option) Unsynchronized.ref
-  val test_term: Proof.context -> term -> int -> term list option * (bool list * bool)
+  val test_term: Proof.context -> term -> int -> term list option
   val eval_result: (unit -> term) Unsynchronized.ref
   val eval_term: theory -> term -> term
   val evaluation_conv: cterm -> thm
@@ -895,8 +895,7 @@
           str ");"]) ^
       "\n\nend;\n";
     val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
-    val dummy_report = ([], false)
-  in (fn size => (! test_fn size, dummy_report)) end;
+  in (fn size => (! test_fn size)) end;
 
 
 
--- a/src/Pure/library.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/Pure/library.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -727,7 +727,7 @@
 (*simple quoting (does not escape special chars)*)
 val quote = enclose "\"" "\"";
 
-(*space_implode "..." (explode "hello") = "h...e...l...l...o"*)
+(*space_implode "..." (Symbol.explode "hello") = "h...e...l...l...o"*)
 fun space_implode a bs = implode (separate a bs);
 
 val commas = space_implode ", ";
--- a/src/Tools/auto_tools.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/Tools/auto_tools.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -6,10 +6,11 @@
 
 signature AUTO_TOOLS =
 sig
-  val time_limit: int Unsynchronized.ref
+  val time_limit: real Unsynchronized.ref
 
   val register_tool :
-    string * (Proof.state -> bool * Proof.state) -> theory -> theory
+    bool Unsynchronized.ref * (Proof.state -> bool * Proof.state) -> theory
+    -> theory
 end;
 
 structure Auto_Tools : AUTO_TOOLS =
@@ -17,20 +18,20 @@
 
 (* preferences *)
 
-val time_limit = Unsynchronized.ref 4000
+val time_limit = Unsynchronized.ref 4.0
 
+val auto_tools_time_limitN = "auto-tools-time-limit"
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_tracing
-    (Preferences.nat_pref time_limit
-      "auto-tools-time-limit"
-      "Time limit for automatic tools (in milliseconds).")
+    (Preferences.real_pref time_limit
+      auto_tools_time_limitN "Time limit for automatic tools (in seconds).")
 
 
 (* configuration *)
 
 structure Data = Theory_Data
 (
-  type T = (string * (Proof.state -> bool * Proof.state)) list
+  type T = (bool Unsynchronized.ref * (Proof.state -> bool * Proof.state)) list
   val empty = []
   val extend = I
   fun merge data : T = AList.merge (op =) (K true) data
@@ -41,18 +42,30 @@
 
 (* automatic testing *)
 
+fun run_tools tools state =
+  tools |> map_filter (fn (auto, tool) => if !auto then SOME tool else NONE)
+        |> Par_List.get_some (fn tool =>
+                                 case try tool state of
+                                   SOME (true, state) => SOME state
+                                 | _ => NONE)
+        |> the_default state
+
+(* Too large values are understood as milliseconds, ensuring compatibility with
+   old setting files. No users can possibly in their right mind want the user
+   interface to block for more than 100 seconds. *)
+fun smart_seconds r =
+  seconds (if r >= 100.0 then
+             (legacy_feature (quote auto_tools_time_limitN ^
+                " expressed in milliseconds -- use seconds instead"); 0.001 * r)
+           else
+             r)
+
 val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
-  case !time_limit of
-    0 => state
-  | ms =>
-    TimeLimit.timeLimit (Time.fromMilliseconds ms)
-        (fn () =>
-            if interact andalso not (!Toplevel.quiet) then
-              fold_rev (fn (_, tool) => fn (true, state) => (true, state)
-                                         | (false, state) => tool state)
-                   (Data.get (Proof.theory_of state)) (false, state) |> snd
-            else
-              state) ()
-    handle TimeLimit.TimeOut => state))
+  if interact andalso not (!Toplevel.quiet) andalso !time_limit > 0.0 then
+    TimeLimit.timeLimit (smart_seconds (!time_limit))
+        (run_tools (Data.get (Proof.theory_of state))) state
+    handle TimeLimit.TimeOut => state
+  else
+    state))
 
 end;
--- a/src/Tools/quickcheck.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/Tools/quickcheck.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -10,6 +10,7 @@
   (* configuration *)
   val auto: bool Unsynchronized.ref
   val timing : bool Unsynchronized.ref
+  val tester : string Config.T 
   val size : int Config.T
   val iterations : int Config.T
   val no_assms : bool Config.T
@@ -27,16 +28,14 @@
   val map_test_params : (typ list * expectation -> typ list * expectation)
     -> Context.generic -> Context.generic
   val add_generator:
-    string * (Proof.context -> term -> int -> term list option * (bool list * bool))
+    string * (Proof.context -> term -> int -> term list option * report option)
       -> Context.generic -> Context.generic
   (* testing terms and proof states *)
-  val test_term_small: Proof.context -> term ->
-    (string * term) list option * ((string * int) list * ((int * report list) list) option)
-  val test_term: Proof.context -> string option -> term ->
-    (string * term) list option * ((string * int) list * ((int * report list) list) option)
+  val test_term: Proof.context -> bool -> term ->
+    (string * term) list option * ((string * int) list * ((int * report) list) option)
   val test_goal_terms:
-    Proof.context -> string option * (string * typ) list -> term list
-      -> (string * term) list option * ((string * int) list * ((int * report list) list) option) list
+    Proof.context -> bool -> (string * typ) list -> term list
+      -> (string * term) list option * ((string * int) list * ((int * report) list) option) list
   val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
 end;
 
@@ -58,26 +57,10 @@
 
 (* quickcheck report *)
 
-datatype single_report = Run of bool list * bool | MatchExc
-
 datatype report = Report of
   { iterations : int, raised_match_errors : int,
     satisfied_assms : int list, positive_concl_tests : int }
 
-fun collect_single_report single_report
-    (Report {iterations = iterations, raised_match_errors = raised_match_errors,
-    satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
-  case single_report
-  of MatchExc =>
-    Report {iterations = iterations + 1, raised_match_errors = raised_match_errors + 1,
-      satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}
-   | Run (assms, concl) =>
-    Report {iterations = iterations + 1, raised_match_errors = raised_match_errors,
-      satisfied_assms =
-        map2 (fn b => fn s => if b then s + 1 else s) assms
-         (if null satisfied_assms then replicate (length assms) 0 else satisfied_assms),
-      positive_concl_tests = if concl then positive_concl_tests + 1 else positive_concl_tests}
-
 (* expectation *)
 
 datatype expectation = No_Expectation | No_Counterexample | Counterexample; 
@@ -86,6 +69,7 @@
   if expect1 = expect2 then expect1 else No_Expectation
 
 (* quickcheck configuration -- default parameters, test generators *)
+val (tester, setup_tester) = Attrib.config_string "quickcheck_tester" (K "")
 val (size, setup_size) = Attrib.config_int "quickcheck_size" (K 10)
 val (iterations, setup_iterations) = Attrib.config_int "quickcheck_iterations" (K 100)
 val (no_assms, setup_no_assms) = Attrib.config_bool "quickcheck_no_assms" (K false)
@@ -96,8 +80,8 @@
 val (finite_type_size, setup_finite_type_size) = Attrib.config_int "quickcheck_finite_type_size" (K 3)
 
 val setup_config =
-  setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_quiet #> setup_timeout
-    #> setup_finite_types #> setup_finite_type_size
+  setup_tester #> setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_quiet
+    #> setup_timeout #> setup_finite_types #> setup_finite_type_size
 
 datatype test_params = Test_Params of
   {default_type: typ list, expect : expectation};
@@ -116,7 +100,7 @@
 structure Data = Generic_Data
 (
   type T =
-    (string * (Proof.context -> term -> int -> term list option * (bool list * bool))) list
+    (string * (Proof.context -> term -> int -> term list option * report option)) list
       * test_params;
   val empty = ([], Test_Params {default_type = [], expect = No_Expectation});
   val extend = I;
@@ -137,25 +121,23 @@
 
 (* generating tests *)
 
-fun mk_tester_select name ctxt =
-  case AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) name
-   of NONE => error ("No such quickcheck generator: " ^ name)
-    | SOME generator => generator ctxt;
-
-fun mk_testers ctxt t =
-  (map snd o fst o Data.get o Context.Proof) ctxt
-  |> map_filter (fn generator => try (generator ctxt) t);
-
-fun mk_testers_strict ctxt t =
+fun mk_tester ctxt t =
   let
-    val generators = ((map snd o fst o Data.get o Context.Proof) ctxt)
-    val testers = map (fn generator => Exn.interruptible_capture (generator ctxt) t) generators;
+    val name = Config.get ctxt tester
+    val tester = case AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) name
+      of NONE => error ("No such quickcheck tester: " ^ name)
+      | SOME tester => tester ctxt;
   in
-    if forall (is_none o Exn.get_result) testers
-    then [(Exn.release o snd o split_last) testers]
-    else map_filter Exn.get_result testers
-  end;
-
+    if Config.get ctxt quiet then
+      try tester t
+    else
+      let
+        val tester = Exn.interruptible_capture tester t
+      in case Exn.get_result tester of
+          NONE => SOME (Exn.release tester)
+        | SOME tester => SOME tester
+      end
+  end
 
 (* testing propositions *)
 
@@ -174,96 +156,40 @@
     val result = Exn.capture f ()
     val time = Time.toMilliseconds (#cpu (end_timing start))
   in (Exn.release result, (description, time)) end
-
-fun test_term_small ctxt t =
-  let
-    val (names, t') = prep_test_term t;
-    val current_size = Unsynchronized.ref 0
-    fun excipit s =
-      "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
-    val (tester, comp_time) = cpu_time "compilation"
-      (fn () => the (AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) "small") ctxt t');
-    val empty_report = Report { iterations = 0, raised_match_errors = 0,
-      satisfied_assms = [], positive_concl_tests = 0 }
-    fun with_size k timings =
-      if k > Config.get ctxt size then (NONE, timings)
-      else
-         let
-           val _ = if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
-           val _ = current_size := k
-           val (result, timing) = cpu_time ("size " ^ string_of_int k)
-             (fn () => (fst (tester k)) handle Match => (if Config.get ctxt quiet then ()
-             else warning "Exception Match raised during quickcheck"; NONE))
-        in
-          case result of
-            NONE => with_size (k + 1) (timing :: timings)
-          | SOME q => (SOME q, (timing :: timings))
-        end;
-     val result = with_size 1 [comp_time]
-   in
-     apsnd (rpair NONE) (apfst (Option.map (curry (op ~~) names)) result)
-   end
-
-(* we actually assume we know the generators and its behaviour *)
-fun is_iteratable "SML" = true
-  | is_iteratable "random" = true
-  | is_iteratable _ = false
   
-fun test_term ctxt generator_name t =
+fun test_term ctxt is_interactive t =
   let
     val (names, t') = prep_test_term t;
     val current_size = Unsynchronized.ref 0
     fun excipit s =
       "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
-    val (testers, comp_time) = cpu_time "quickcheck compilation"
-      (fn () => (case generator_name
-       of NONE => if Config.get ctxt quiet then mk_testers ctxt t' else mk_testers_strict ctxt t'
-        | SOME name => [mk_tester_select name ctxt t']));
-    fun iterate f 0 report = (NONE, report)
-      | iterate f j report =
-        let
-          val (test_result, single_report) = apsnd Run (f ()) handle Match => 
-            (if Config.get ctxt quiet then ()
-             else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
-          val report = collect_single_report single_report report
-        in
-          case test_result of NONE => iterate f (j - 1) report | SOME q => (SOME q, report)
-        end
-    val empty_report = Report { iterations = 0, raised_match_errors = 0,
-      satisfied_assms = [], positive_concl_tests = 0 }
-    fun with_testers k [] = (NONE, [])
-      | with_testers k (tester :: testers) =
+    val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt t');
+    fun with_size test_fun k reports =
+      if k > Config.get ctxt size then
+        (NONE, reports)
+      else
         let
-          val niterations = case generator_name of
-            SOME generator_name =>
-              if is_iteratable generator_name then Config.get ctxt iterations else 1
-          | NONE => Config.get ctxt iterations
-          val (result, timing) = cpu_time ("size " ^ string_of_int k)
-            (fn () => iterate (fn () => tester (k - 1)) niterations empty_report)
-        in
-          case result
-           of (NONE, report) => apsnd (cons report) (with_testers k testers)
-            | (SOME q, report) => (SOME q, [report])
-        end
-    fun with_size k reports =
-      if k > Config.get ctxt size then (NONE, reports)
-      else
-       (if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
-        let
+          val _ = if Config.get ctxt quiet then () else Output.urgent_message
+            ("Test data size: " ^ string_of_int k)
           val _ = current_size := k
-          val (result, new_report) = with_testers k testers
-          val reports = ((k, new_report) :: reports)
-        in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end);
-    val ((result, reports), exec_time) =
-      TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () => cpu_time "quickcheck execution"
-      (fn () => apfst
-         (fn result => case result of NONE => NONE
-        | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
-      handle TimeLimit.TimeOut =>
-        error (excipit "ran out of time")
-     | Exn.Interrupt => error (excipit "was interrupted")  (* FIXME violates Isabelle/ML exception model *)
+          val ((result, new_report), timing) =
+            cpu_time ("size " ^ string_of_int k) (fn () => test_fun (k - 1))
+          val reports = case new_report of NONE => reports | SOME rep => (k, rep) :: reports
+        in case result of NONE => with_size test_fun (k + 1) reports | SOME q => (SOME q, reports) end;
   in
-    (result, ([exec_time, comp_time], if Config.get ctxt report then SOME reports else NONE))
+    case test_fun of NONE => (NONE, ([comp_time], NONE)) 
+      | SOME test_fun =>
+        TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () =>
+          let
+            val ((result, reports), exec_time) =
+              cpu_time "quickcheck execution" (fn () => with_size test_fun 1 [])
+          in
+            (case result of NONE => NONE | SOME ts => SOME (names ~~ ts),
+              ([exec_time, comp_time],
+               if Config.get ctxt report andalso not (null reports) then SOME reports else NONE))
+          end) ()
+        handle TimeLimit.TimeOut =>
+          if is_interactive then error (excipit "ran out of time") else raise TimeLimit.TimeOut
   end;
 
 fun get_finite_types ctxt =
@@ -276,33 +202,34 @@
 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
+      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
 
-fun test_goal_terms lthy (generator_name, insts) check_goals =
+fun test_goal_terms lthy is_interactive insts check_goals =
   let
     val thy = ProofContext.theory_of lthy 
+    val default_insts =
+      if Config.get lthy finite_types then (get_finite_types lthy) else (default_type lthy)
     val inst_goals =
-      if Config.get lthy finite_types then 
-        maps (fn check_goal => map (fn T =>
-          Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
-            handle WELLSORTED s => Wellsorted_Error s) (get_finite_types lthy)) check_goals
-      else
-        maps (fn check_goal => map (fn T =>
-          Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
-            handle WELLSORTED s => Wellsorted_Error s) (default_type lthy)) check_goals
+      maps (fn check_goal =>
+        if not (null (Term.add_tfree_names check_goal [])) then
+          map (fn T =>
+            ((Term o Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
+              handle WELLSORTED s => Wellsorted_Error s) default_insts 
+        else
+          [Term (Object_Logic.atomize_term thy check_goal)]) check_goals
     val error_msg = cat_lines (map_filter (fn Term t => NONE | Wellsorted_Error s => SOME s) inst_goals)
     val correct_inst_goals =
       case map_filter (fn Term t => SOME t | Wellsorted_Error s => NONE) inst_goals of
@@ -314,9 +241,9 @@
         case f t of
           (SOME res, report) => (SOME res, rev (report :: reports))
         | (NONE, report) => collect_results f (report :: reports) ts
-  in collect_results (test_term lthy generator_name) [] correct_inst_goals end;
+  in collect_results (test_term lthy is_interactive) [] correct_inst_goals end;
 
-fun test_goal (generator_name, insts) i state =
+fun test_goal insts i state =
   let
     val lthy = Proof.context_of state;
     val thy = Proof.theory_of state;
@@ -337,7 +264,7 @@
       | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal)
         (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
   in
-    test_goal_terms lthy (generator_name, insts) check_goals
+    test_goal_terms lthy true insts check_goals
   end
 
 (* pretty printing *)
@@ -348,7 +275,7 @@
   | pretty_counterex ctxt auto (SOME cex) =
       Pretty.chunks (Pretty.str (tool_name auto ^ " found a counterexample:\n") ::
         map (fn (s, t) =>
-          Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
+          Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex));
 
 fun pretty_report (Report {iterations = iterations, raised_match_errors = raised_match_errors,
     satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
@@ -362,16 +289,10 @@
      @ [pretty_stat "positive conclusion tests" positive_concl_tests])
   end
 
-fun pretty_reports' [report] = [Pretty.chunks (pretty_report report)]
-  | pretty_reports' reports =
-  map_index (fn (i, report) =>
-    Pretty.chunks (Pretty.str (string_of_int (i + 1) ^ ". generator:\n") :: pretty_report report))
-    reports
-
 fun pretty_reports ctxt (SOME reports) =
-  Pretty.chunks (Pretty.str "Quickcheck report:" ::
-    maps (fn (size, reports) =>
-      Pretty.str ("size " ^ string_of_int size ^ ":") :: pretty_reports' reports @ [Pretty.brk 1])
+  Pretty.chunks (Pretty.fbrk :: Pretty.str "Quickcheck report:" ::
+    maps (fn (size, report) =>
+      Pretty.str ("size " ^ string_of_int size ^ ":") :: pretty_report report @ [Pretty.brk 1])
       (rev reports))
   | pretty_reports ctxt NONE = Pretty.str ""
 
@@ -382,24 +303,21 @@
 (* automatic testing *)
 
 fun auto_quickcheck state =
-  if not (!auto) then
-    (false, state)
-  else
-    let
-      val ctxt = Proof.context_of state;
-      val res =
-        state
-        |> Proof.map_context (Config.put report false #> Config.put quiet true)
-        |> try (test_goal (NONE, []) 1);
-    in
-      case res of
-        NONE => (false, state)
-      | SOME (NONE, report) => (false, state)
-      | SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
-          Pretty.mark Markup.hilite (pretty_counterex ctxt true cex)])) state)
-    end
+  let
+    val ctxt = Proof.context_of state;
+    val res =
+      state
+      |> Proof.map_context (Config.put report false #> Config.put quiet true)
+      |> try (test_goal [] 1);
+  in
+    case res of
+      NONE => (false, state)
+    | SOME (NONE, report) => (false, state)
+    | SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
+        Pretty.mark Markup.hilite (pretty_counterex ctxt true cex)])) state)
+  end
 
-val setup = Auto_Tools.register_tool ("quickcheck", auto_quickcheck)
+val setup = Auto_Tools.register_tool (auto, auto_quickcheck)
   #> setup_config
 
 (* Isar commands *)
@@ -423,7 +341,16 @@
   | read_expectation "counterexample" = Counterexample
   | read_expectation s = error ("Not an expectation value: " ^ s)  
 
-fun parse_test_param ("size", [arg]) = Config.put_generic size (read_nat arg)
+fun valid_tester_name genctxt = AList.defined (op =) (fst (Data.get genctxt))
+
+fun parse_tester name genctxt =
+  if valid_tester_name genctxt name then
+    Config.put_generic tester name genctxt
+  else
+    error ("Unknown tester: " ^ name)
+
+fun parse_test_param ("tester", [arg]) = parse_tester arg
+  | parse_test_param ("size", [arg]) = Config.put_generic size (read_nat arg)
   | parse_test_param ("iterations", [arg]) = Config.put_generic iterations (read_nat arg)
   | parse_test_param ("default_type", arg) = (fn gen_ctxt =>
     map_test_params ((apfst o K) (map (ProofContext.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt)
@@ -434,22 +361,23 @@
   | parse_test_param ("timeout", [arg]) = Config.put_generic timeout (read_real arg)
   | parse_test_param ("finite_types", [arg]) = Config.put_generic finite_types (read_bool arg)
   | parse_test_param ("finite_type_size", [arg]) = Config.put_generic finite_type_size (read_nat arg)
-  | parse_test_param (name, _) = error ("Unknown test parameter: " ^ name);
+  | parse_test_param (name, _) = fn genctxt =>
+    if valid_tester_name genctxt name then
+      Config.put_generic tester name genctxt
+    else error ("Unknown tester or test parameter: " ^ name);
 
-fun parse_test_param_inst ("generator", [arg]) ((generator, insts), ctxt) =
-      (apfst o apfst o K o SOME) arg ((generator, insts), ctxt)
-  | parse_test_param_inst (name, arg) ((generator, insts), ctxt) =
+fun parse_test_param_inst (name, arg) (insts, ctxt) =
       case try (ProofContext.read_typ ctxt) name
-       of SOME (TFree (v, _)) => (apfst o apsnd o AList.update (op =))
-              (v, ProofContext.read_typ ctxt (the_single arg)) ((generator, insts), ctxt)
-        | _ => (apsnd o Context.proof_map o parse_test_param) (name, arg) ((generator, insts), ctxt);
+       of SOME (TFree (v, _)) => (apfst o AList.update (op =))
+              (v, ProofContext.read_typ ctxt (the_single arg)) (insts, ctxt)
+        | _ => (apsnd o Context.proof_map o parse_test_param) (name, arg) (insts, ctxt);
 
 fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
   
 fun gen_quickcheck args i state =
   state
-  |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ((NONE, []), ctxt))
-  |> (fn ((generator, insts), state') => test_goal (generator, insts) i state'
+  |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ([], ctxt))
+  |> (fn (insts, state') => test_goal insts i state'
   |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
                error ("quickcheck expected to find no counterexample but found one") else ()
            | (NONE, _) => if expect (Proof.context_of state') = Counterexample then
--- a/src/Tools/solve_direct.ML	Fri Dec 03 17:16:53 2010 +0100
+++ b/src/Tools/solve_direct.ML	Fri Dec 03 17:18:41 2010 +0100
@@ -97,9 +97,8 @@
 
 (* hook *)
 
-fun auto_solve_direct state =
-  if not (! auto) then (false, state) else solve_direct true state;
+val auto_solve_direct = solve_direct true
 
-val setup = Auto_Tools.register_tool (solve_directN, auto_solve_direct);
+val setup = Auto_Tools.register_tool (auto, auto_solve_direct);
 
 end;