1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Mon Jul 18 10:34:21 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Mon Jul 18 10:34:21 2011 +0200
     1.3 @@ -452,7 +452,7 @@
     1.4  
     1.5  setup {* Exhaustive_Generators.setup *}
     1.6  
     1.7 -declare [[quickcheck_tester = exhaustive]]
     1.8 +declare [[quickcheck_batch_tester = exhaustive]]
     1.9  
    1.10  hide_fact orelse_def catch_match_def
    1.11  no_notation orelse (infixr "orelse" 55)

     2.1 --- a/src/Tools/quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
     2.2 +++ b/src/Tools/quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4    val setup: theory -> theory
     2.5    (* configuration *)
     2.6    val auto: bool Unsynchronized.ref
     2.7 -  val tester : string Config.T
     2.8 +  val batch_tester : string Config.T
     2.9    val size : int Config.T
    2.10    val iterations : int Config.T
    2.11    val no_assms : bool Config.T
    2.12 @@ -161,7 +161,7 @@
    2.13    if expect1 = expect2 then expect1 else No_Expectation
    2.14  
    2.15  (* quickcheck configuration -- default parameters, test generators *)
    2.16 -val tester = Attrib.setup_config_string @{binding quickcheck_tester} (K "")
    2.17 +val batch_tester = Attrib.setup_config_string @{binding quickcheck_batch_tester} (K "")
    2.18  val size = Attrib.setup_config_int @{binding quickcheck_size} (K 10)
    2.19  val iterations = Attrib.setup_config_int @{binding quickcheck_iterations} (K 100)
    2.20  val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
    2.21 @@ -244,9 +244,9 @@
    2.22  
    2.23  fun gen_mk_tester lookup ctxt v =
    2.24    let
    2.25 -    val name = Config.get ctxt tester
    2.26 +    val name = Config.get ctxt batch_tester
    2.27      val tester = case lookup ctxt name
    2.28 -      of NONE => error ("No such quickcheck tester: " ^ name)
    2.29 +      of NONE => error ("No such quickcheck batch-tester: " ^ name)
    2.30        | SOME tester => tester ctxt;
    2.31    in
    2.32      if Config.get ctxt quiet then
    2.33 @@ -259,10 +259,7 @@
    2.34          | SOME tester => SOME tester
    2.35        end
    2.36    end
    2.37 -(*
    2.38 -val mk_tester =
    2.39 -  gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o fst o fst o Data.get o Context.Proof) ctxt))
    2.40 -*)
    2.41 +
    2.42  val mk_batch_tester =
    2.43    gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o snd o fst o Data.get o Context.Proof) ctxt))
    2.44  val mk_batch_validator =