--- a/src/HOL/ex/Quickcheck.thy Sun Sep 28 14:46:51 2008 +0200
+++ b/src/HOL/ex/Quickcheck.thy Mon Sep 29 10:58:01 2008 +0200
@@ -157,8 +157,7 @@
|-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
|> snd
|> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
- |> LocalTheory.exit
- |> ProofContext.theory_of
+ |> LocalTheory.exit_global
end
| random_inst tycos thy = raise REC
("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos));