diff -r 548a3e5521ab -r 8f176e575a49 src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Thu Sep 09 14:38:14 2010 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Thu Sep 09 16:43:57 2010 +0200 @@ -404,6 +404,7 @@ val setup = Datatype.interpretation ensure_random_datatype #> Code_Target.extend_target (target, (Code_Eval.target, K I)) - #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of); + #> Context.theory_map + (Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of)); end;