# HG changeset patch
# User bulwahn
# Date 1310978061 -7200
# Node ID 05d5696f177f87b48335a2d81a811ce638b66479
# Parent  cabe74eab19afa2ab2ef8832e2b39c1a1b8e42ca
renaming quickcheck_tester to quickcheck_batch_tester; tuned

diff -r cabe74eab19a -r 05d5696f177f src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Mon Jul 18 10:34:21 2011 +0200
@@ -452,7 +452,7 @@
 
 setup {* Exhaustive_Generators.setup *}
 
-declare [[quickcheck_tester = exhaustive]]
+declare [[quickcheck_batch_tester = exhaustive]]
 
 hide_fact orelse_def catch_match_def
 no_notation orelse (infixr "orelse" 55)
diff -r cabe74eab19a -r 05d5696f177f src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/Tools/quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
@@ -13,7 +13,7 @@
   val setup: theory -> theory
   (* configuration *)
   val auto: bool Unsynchronized.ref
-  val tester : string Config.T
+  val batch_tester : string Config.T
   val size : int Config.T
   val iterations : int Config.T
   val no_assms : bool Config.T
@@ -161,7 +161,7 @@
   if expect1 = expect2 then expect1 else No_Expectation
 
 (* quickcheck configuration -- default parameters, test generators *)
-val tester = Attrib.setup_config_string @{binding quickcheck_tester} (K "")
+val batch_tester = Attrib.setup_config_string @{binding quickcheck_batch_tester} (K "")
 val size = Attrib.setup_config_int @{binding quickcheck_size} (K 10)
 val iterations = Attrib.setup_config_int @{binding quickcheck_iterations} (K 100)
 val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
@@ -244,9 +244,9 @@
 
 fun gen_mk_tester lookup ctxt v =
   let
-    val name = Config.get ctxt tester
+    val name = Config.get ctxt batch_tester
     val tester = case lookup ctxt name
-      of NONE => error ("No such quickcheck tester: " ^ name)
+      of NONE => error ("No such quickcheck batch-tester: " ^ name)
       | SOME tester => tester ctxt;
   in
     if Config.get ctxt quiet then
@@ -259,10 +259,7 @@
         | SOME tester => SOME tester
       end
   end
-(*
-val mk_tester =
-  gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o fst o fst o Data.get o Context.Proof) ctxt))
-*)
+
 val mk_batch_tester =
   gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o snd o fst o Data.get o Context.Proof) ctxt))
 val mk_batch_validator =