1.1 --- a/src/Tools/quickcheck.ML	Thu Feb 20 19:38:34 2014 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Thu Feb 20 19:44:48 2014 +0100
     1.3 @@ -254,13 +254,13 @@
     1.4      map snd (filter (fn (active, _) => Config.get ctxt active) testers)
     1.5    end;
     1.6  
     1.7 -fun set_active_testers [] gen_ctxt = gen_ctxt
     1.8 -  | set_active_testers testers gen_ctxt =
     1.9 +fun set_active_testers [] context = context
    1.10 +  | set_active_testers testers context =
    1.11        let
    1.12 -        val registered_testers = fst (fst (Data.get gen_ctxt));
    1.13 +        val registered_testers = fst (fst (Data.get context));
    1.14        in
    1.15          fold (fn (name, (config, _)) => Config.put_generic config (member (op =) testers name))
    1.16 -          registered_testers gen_ctxt
    1.17 +          registered_testers context
    1.18        end;
    1.19  
    1.20  
    1.21 @@ -459,9 +459,9 @@
    1.22    | parse_test_param ("iterations", [arg]) = apsnd (Config.put_generic iterations (read_nat arg))
    1.23    | parse_test_param ("depth", [arg]) = apsnd (Config.put_generic depth (read_nat arg))
    1.24    | parse_test_param ("default_type", arg) =
    1.25 -      (fn (testers, gen_ctxt) =>
    1.26 +      (fn (testers, context) =>
    1.27          (testers, map_test_params
    1.28 -          (apfst (K (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg))) gen_ctxt))
    1.29 +          (apfst (K (map (Proof_Context.read_typ (Context.proof_of context)) arg))) context))
    1.30    | parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg))
    1.31    | parse_test_param ("expect", [arg]) = apsnd (map_test_params (apsnd (K (read_expectation arg))))
    1.32    | parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg))
    1.33 @@ -500,11 +500,11 @@
    1.34          "eval" => ((insts, eval_terms @ map (Syntax.read_term ctxt) arg), (testers, ctxt))
    1.35        | _ =>
    1.36          ((insts, eval_terms),
    1.37 -          proof_map_result (fn gen_ctxt => parse_test_param (name, arg) (testers, gen_ctxt)) ctxt)));
    1.38 +          proof_map_result (fn context => parse_test_param (name, arg) (testers, context)) ctxt)));
    1.39  
    1.40  fun quickcheck_params_cmd args =
    1.41    Context.theory_map
    1.42 -    (fn gen_ctxt => uncurry set_active_testers (fold parse_test_param args ([], gen_ctxt)));
    1.43 +    (fn context => uncurry set_active_testers (fold parse_test_param args ([], context)));
    1.44  
    1.45  fun check_expectation state results =
    1.46    if is_some results andalso expect (Proof.context_of state) = No_Counterexample then