src/HOL/Tools/datatype_rep_proofs.ML
changeset 21525 1b18b5892dc4
parent 21365 4ee8e2702241
child 22578 b0eb5652f210
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Sun Nov 26 18:07:16 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sun Nov 26 18:07:19 2006 +0100
     1.3 @@ -174,12 +174,10 @@
     1.4          ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names'));
     1.5  
     1.6      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
     1.7 -      setmp InductivePackage.quiet_mode (!quiet_mode)
     1.8 -        (TheoryTarget.init NONE #>
     1.9 -         InductivePackage.add_inductive_i false big_rec_name false true false
    1.10 +      setmp InductivePackage.quiet_mode (! quiet_mode)
    1.11 +        (InductivePackage.add_inductive_global false big_rec_name false true false
    1.12             (map (fn s => (s, SOME UnivT', NoSyn)) rep_set_names') []
    1.13 -           (map (fn x => (("", []), x)) intr_ts) [] #>
    1.14 -         apsnd (ProofContext.theory_of o LocalTheory.exit)) thy1;
    1.15 +           (map (fn x => (("", []), x)) intr_ts) []) thy1;
    1.16  
    1.17      (********************************* typedef ********************************)
    1.18