LocalTheory.exit_global;

--- 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

--- a/src/HOL/Library/RType.thy	Sun Sep 28 14:46:51 2008 +0200
+++ b/src/HOL/Library/RType.thy	Mon Sep 29 10:58:01 2008 +0200
@@ -70,8 +70,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;
 
 fun perhaps_add_def tyco thy =

--- a/src/HOL/Statespace/state_space.ML	Sun Sep 28 14:46:51 2008 +0200
+++ b/src/HOL/Statespace/state_space.ML	Mon Sep 29 10:58:01 2008 +0200
@@ -352,8 +352,7 @@
   thy
   |> TheoryTarget.init name
   |> (fn lthy => LocalTheory.declaration (decl lthy) lthy)
-  |> LocalTheory.exit
-  |> ProofContext.theory_of;
+  |> LocalTheory.exit_global;
 
 fun parent_components thy (Ts, pname, renaming) =
   let

--- a/src/HOL/Tools/datatype_codegen.ML	Sun Sep 28 14:46:51 2008 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Mon Sep 29 10:58:01 2008 +0200
@@ -471,8 +471,7 @@
     |> TheoryTarget.instantiation (dtcos, vs', [HOLogic.class_eq])
     |> fold_map add_def dtcos
     |-> (fn thms => Class.prove_instantiation_instance (K (tac thms))
-    #> LocalTheory.exit
-    #> ProofContext.theory_of
+    #> LocalTheory.exit_global
     #> fold Code.del_eqn thms
     #> fold add_eq_thms dtcos)
   end;

--- a/src/HOL/Tools/function_package/size.ML	Sun Sep 28 14:46:51 2008 +0200
+++ b/src/HOL/Tools/function_package/size.ML	Mon Sep 29 10:58:01 2008 +0200
@@ -151,8 +151,7 @@
       ||>> fold_map define_overloaded
         (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
       ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
-      ||> LocalTheory.exit
-      ||> ProofContext.theory_of;
+      ||> LocalTheory.exit_global;
 
     val ctxt = ProofContext.init thy';
 

--- a/src/HOL/Tools/primrec_package.ML	Sun Sep 28 14:46:51 2008 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Mon Sep 29 10:58:01 2008 +0200
@@ -279,14 +279,14 @@
     val lthy = TheoryTarget.init NONE thy;
     val (simps, lthy') = add_primrec fixes specs lthy;
     val simps' = ProofContext.export lthy' lthy simps;
-  in (simps', ProofContext.theory_of (LocalTheory.exit lthy')) end;
+  in (simps', LocalTheory.exit_global lthy') end;
 
 fun add_primrec_overloaded ops fixes specs thy =
   let
     val lthy = TheoryTarget.overloading ops thy;
     val (simps, lthy') = add_primrec fixes specs lthy;
     val simps' = ProofContext.export lthy' lthy simps;
-  in (simps', ProofContext.theory_of (LocalTheory.exit lthy')) end;
+  in (simps', LocalTheory.exit_global lthy') end;
 
 
 (* outer syntax *)

--- a/src/HOL/Tools/typecopy_package.ML	Sun Sep 28 14:46:51 2008 +0200
+++ b/src/HOL/Tools/typecopy_package.ML	Mon Sep 29 10:58:01 2008 +0200
@@ -161,8 +161,7 @@
     |> TheoryTarget.instantiation ([tyco], vs', [HOLogic.class_eq])
     |> add_def tyco
     |-> (fn thm => Class.prove_instantiation_instance (K (tac [thm]))
-    #> LocalTheory.exit
-    #> ProofContext.theory_of
+    #> LocalTheory.exit_global
     #> Code.del_eqn thm
     #> add_eq_thms)
   end;

--- a/src/HOL/Typedef.thy	Sun Sep 28 14:46:51 2008 +0200
+++ b/src/HOL/Typedef.thy	Mon Sep 29 10:58:01 2008 +0200
@@ -148,8 +148,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
 in TypedefPackage.interpretation add_itself end
 *}

--- 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));

--- a/src/HOLCF/Tools/pcpodef_package.ML	Sun Sep 28 14:46:51 2008 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Mon Sep 29 10:58:01 2008 +0200
@@ -100,8 +100,7 @@
         val thy5 = lthy4
           |> Class.prove_instantiation_instance
               (K (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1))
-          |> LocalTheory.exit
-          |> ProofContext.theory_of;
+          |> LocalTheory.exit_global;
       in ((type_definition, less_definition, set_def), thy5) end;
 
     fun make_cpo admissible (type_def, less_def, set_def) theory =

--- a/src/Pure/Isar/toplevel.ML	Sun Sep 28 14:46:51 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Sep 29 10:58:01 2008 +0200
@@ -109,7 +109,7 @@
 type generic_theory = Context.generic;    (*theory or local_theory*)
 
 val loc_init = TheoryTarget.context;
-val loc_exit = ProofContext.theory_of o LocalTheory.exit;
+val loc_exit = LocalTheory.exit_global;
 
 fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
   | loc_begin NONE (Context.Proof lthy) = lthy