diff -r 8f176e575a49 -r 0c47d615a69b src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Thu Sep 09 16:43:57 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Sep 09 17:23:03 2010 +0200
@@ -14,7 +14,7 @@
     -> (string * sort -> string * sort) option
   val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
   val compile_generator_expr:
-    theory -> bool -> term -> int -> term list option * (bool list * bool)
+    Proof.context -> term -> int -> term list option * (bool list * bool)
   val eval_ref: (unit -> int -> seed -> term list option * seed) option Unsynchronized.ref
   val eval_report_ref:
     (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) option Unsynchronized.ref
@@ -380,10 +380,11 @@
     Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check))
   end
 
-fun compile_generator_expr thy report t =
+fun compile_generator_expr ctxt t =
   let
     val Ts = (map snd o fst o strip_abs) t;
-  in if report then
+    val thy = ProofContext.theory_of ctxt
+  in if Quickcheck.report ctxt then
     let
       val t' = mk_reporting_generator_expr thy t Ts;
       val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_report_ref", eval_report_ref)
@@ -405,6 +406,6 @@
   Datatype.interpretation ensure_random_datatype
   #> Code_Target.extend_target (target, (Code_Eval.target, K I))
   #> Context.theory_map
-    (Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of));
+    (Quickcheck.add_generator ("code", compile_generator_expr));
 
 end;