InductivePackage.add_inductive_global;

--- a/src/HOL/Tools/datatype_abs_proofs.ML	Sun Nov 26 18:07:16 2006 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sun Nov 26 18:07:19 2006 +0100
@@ -159,12 +159,10 @@
 
     val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
       setmp InductivePackage.quiet_mode (!quiet_mode)
-        (TheoryTarget.init NONE #>
-         InductivePackage.add_inductive_i false big_rec_name' false false true
+        (InductivePackage.add_inductive_global false big_rec_name' false false true
            (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) [] #>
-         apsnd (ProofContext.theory_of o LocalTheory.exit)) thy0;
+           (map (fn x => (("", []), x)) rec_intr_ts) []) thy0;
 
     (* prove uniqueness and termination of primrec combinators *)
 

--- a/src/HOL/Tools/datatype_rep_proofs.ML	Sun Nov 26 18:07:16 2006 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sun Nov 26 18:07:19 2006 +0100
@@ -174,12 +174,10 @@
         ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names'));
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
-      setmp InductivePackage.quiet_mode (!quiet_mode)
-        (TheoryTarget.init NONE #>
-         InductivePackage.add_inductive_i false big_rec_name false true false
+      setmp InductivePackage.quiet_mode (! quiet_mode)
+        (InductivePackage.add_inductive_global false big_rec_name false true false
            (map (fn s => (s, SOME UnivT', NoSyn)) rep_set_names') []
-           (map (fn x => (("", []), x)) intr_ts) [] #>
-         apsnd (ProofContext.theory_of o LocalTheory.exit)) thy1;
+           (map (fn x => (("", []), x)) intr_ts) []) thy1;
 
     (********************************* typedef ********************************)