simplified LocalTheory.exit;

--- a/src/HOL/Nominal/nominal_package.ML	Fri Nov 10 20:58:48 2006 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Fri Nov 10 22:18:51 2006 +0100
@@ -520,7 +520,7 @@
            (map (fn (s, T) => (s, SOME (T --> HOLogic.boolT), NoSyn))
               (rep_set_names' ~~ recTs'))
            [] (map (fn x => (("", []), x)) intr_ts) [] #>
-         apfst (snd o LocalTheory.exit false)) thy3;
+         apfst (ProofContext.theory_of o LocalTheory.exit)) thy3;
 
     (**** Prove that representing set is closed under permutation ****)
 
@@ -1448,7 +1448,7 @@
            (map (fn (s, T) => (s, SOME T, NoSyn)) (rec_set_names' ~~ rec_set_Ts))
            (map (apsnd SOME o dest_Free) rec_fns)
            (map (fn x => (("", []), x)) rec_intr_ts) [] #>
-         apfst (snd o LocalTheory.exit false)) |>>
+         apfst (ProofContext.theory_of o LocalTheory.exit)) |>>
       PureThy.hide_thms true [NameSpace.append
         (Sign.full_name thy10 big_rec_name) "induct"];
 

--- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Nov 10 20:58:48 2006 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Nov 10 22:18:51 2006 +0100
@@ -164,7 +164,7 @@
            (map (fn (s, T) => (s, SOME T, NoSyn)) (rec_set_names' ~~ rec_set_Ts))
            (map (apsnd SOME o dest_Free) rec_fns)
            (map (fn x => (("", []), x)) rec_intr_ts) [] #>
-         apfst (snd o LocalTheory.exit false)) thy0;
+         apfst (ProofContext.theory_of o LocalTheory.exit)) thy0;
 
     (* prove uniqueness and termination of primrec combinators *)
 

--- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Nov 10 20:58:48 2006 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Nov 10 22:18:51 2006 +0100
@@ -179,7 +179,7 @@
          InductivePackage.add_inductive_i false big_rec_name false true false
            (map (fn s => (s, SOME UnivT', NoSyn)) rep_set_names') []
            (map (fn x => (("", []), x)) intr_ts) [] #>
-         apfst (snd o LocalTheory.exit false)) thy1;
+         apfst (ProofContext.theory_of o LocalTheory.exit)) thy1;
 
     (********************************* typedef ********************************)