src/Tools/quickcheck.ML

--- a/src/Tools/quickcheck.ML	Thu Feb 20 19:38:34 2014 +0100
+++ b/src/Tools/quickcheck.ML	Thu Feb 20 19:44:48 2014 +0100
@@ -254,13 +254,13 @@
     map snd (filter (fn (active, _) => Config.get ctxt active) testers)
   end;
 
-fun set_active_testers [] gen_ctxt = gen_ctxt
-  | set_active_testers testers gen_ctxt =
+fun set_active_testers [] context = context
+  | set_active_testers testers context =
       let
-        val registered_testers = fst (fst (Data.get gen_ctxt));
+        val registered_testers = fst (fst (Data.get context));
       in
         fold (fn (name, (config, _)) => Config.put_generic config (member (op =) testers name))
-          registered_testers gen_ctxt
+          registered_testers context
       end;
 
 
@@ -459,9 +459,9 @@
   | parse_test_param ("iterations", [arg]) = apsnd (Config.put_generic iterations (read_nat arg))
   | parse_test_param ("depth", [arg]) = apsnd (Config.put_generic depth (read_nat arg))
   | parse_test_param ("default_type", arg) =
-      (fn (testers, gen_ctxt) =>
+      (fn (testers, context) =>
         (testers, map_test_params
-          (apfst (K (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg))) gen_ctxt))
+          (apfst (K (map (Proof_Context.read_typ (Context.proof_of context)) arg))) context))
   | parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg))
   | parse_test_param ("expect", [arg]) = apsnd (map_test_params (apsnd (K (read_expectation arg))))
   | parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg))
@@ -500,11 +500,11 @@
         "eval" => ((insts, eval_terms @ map (Syntax.read_term ctxt) arg), (testers, ctxt))
       | _ =>
         ((insts, eval_terms),
-          proof_map_result (fn gen_ctxt => parse_test_param (name, arg) (testers, gen_ctxt)) ctxt)));
+          proof_map_result (fn context => parse_test_param (name, arg) (testers, context)) ctxt)));
 
 fun quickcheck_params_cmd args =
   Context.theory_map
-    (fn gen_ctxt => uncurry set_active_testers (fold parse_test_param args ([], gen_ctxt)));
+    (fn context => uncurry set_active_testers (fold parse_test_param args ([], context)));
 
 fun check_expectation state results =
   if is_some results andalso expect (Proof.context_of state) = No_Counterexample then