
diff -r 548a3e5521ab -r 8f176e575a49 src/HOL/Library/SML_Quickcheck.thy
--- a/src/HOL/Library/SML_Quickcheck.thy	Thu Sep 09 14:38:14 2010 +0200
+++ b/src/HOL/Library/SML_Quickcheck.thy	Thu Sep 09 16:43:57 2010 +0200
@@ -7,7 +7,7 @@
 
 setup {*
   Inductive_Codegen.quickcheck_setup #>
-  Quickcheck.add_generator ("SML", Codegen.test_term)
+  Context.theory_map (Quickcheck.add_generator ("SML", Codegen.test_term))
 *}
 
 end




