src/HOL/Tools/quickcheck_generators.ML
changeset 39252 8f176e575a49
parent 38786 e46e7a9cb622
child 39253 0c47d615a69b
--- 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;