diff -r 50f155005ea0 -r 47286c847749 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Thu Feb 20 19:44:48 2014 +0100
+++ b/src/Tools/quickcheck.ML	Thu Feb 20 19:52:43 2014 +0100
@@ -488,8 +488,6 @@
           (insert (op =) name testers, genctxt)
         else error ("Unknown tester or test parameter: " ^ name));
 
-fun proof_map_result f = apsnd Context.the_proof o f o Context.Proof;
-
 fun parse_test_param_inst (name, arg) ((insts, eval_terms), (testers, ctxt)) =
   (case try (Proof_Context.read_typ ctxt) name of
     SOME (TFree (v, _)) =>
@@ -500,7 +498,10 @@
         "eval" => ((insts, eval_terms @ map (Syntax.read_term ctxt) arg), (testers, ctxt))
       | _ =>
         ((insts, eval_terms),
-          proof_map_result (fn context => parse_test_param (name, arg) (testers, context)) ctxt)));
+          let
+            val (testers', Context.Proof ctxt') =
+              parse_test_param (name, arg) (testers, Context.Proof ctxt);
+          in (testers', ctxt') end)));
 
 fun quickcheck_params_cmd args =
   Context.theory_map