src/HOL/Code_Eval.thy

--- a/src/HOL/Code_Eval.thy	Sun Sep 28 14:46:51 2008 +0200
+++ b/src/HOL/Code_Eval.thy	Mon Sep 29 10:58:01 2008 +0200
@@ -70,8 +70,7 @@
       |-> (fn eq => Specification.definition (NONE, ((Name.binding (triv_name_of eq), []), eq)))
       |> snd
       |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
-      |> LocalTheory.exit
-      |> ProofContext.theory_of
+      |> LocalTheory.exit_global
     end;
   fun interpretator (tyco, (raw_vs, _)) thy =
     let