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