InductivePackage.add_inductive_global;
authorwenzelm
Sun Nov 26 18:07:19 2006 +0100 (2006-11-26)
changeset 215251b18b5892dc4
parent 21524 7843e2fd14a9
child 21526 1e6bd5ed7abc
InductivePackage.add_inductive_global;
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Sun Nov 26 18:07:16 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sun Nov 26 18:07:19 2006 +0100
     1.3 @@ -159,12 +159,10 @@
     1.4  
     1.5      val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
     1.6        setmp InductivePackage.quiet_mode (!quiet_mode)
     1.7 -        (TheoryTarget.init NONE #>
     1.8 -         InductivePackage.add_inductive_i false big_rec_name' false false true
     1.9 +        (InductivePackage.add_inductive_global false big_rec_name' false false true
    1.10             (map (fn (s, T) => (s, SOME T, NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    1.11             (map (apsnd SOME o dest_Free) rec_fns)
    1.12 -           (map (fn x => (("", []), x)) rec_intr_ts) [] #>
    1.13 -         apsnd (ProofContext.theory_of o LocalTheory.exit)) thy0;
    1.14 +           (map (fn x => (("", []), x)) rec_intr_ts) []) thy0;
    1.15  
    1.16      (* prove uniqueness and termination of primrec combinators *)
    1.17  
     2.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Sun Nov 26 18:07:16 2006 +0100
     2.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sun Nov 26 18:07:19 2006 +0100
     2.3 @@ -174,12 +174,10 @@
     2.4          ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names'));
     2.5  
     2.6      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
     2.7 -      setmp InductivePackage.quiet_mode (!quiet_mode)
     2.8 -        (TheoryTarget.init NONE #>
     2.9 -         InductivePackage.add_inductive_i false big_rec_name false true false
    2.10 +      setmp InductivePackage.quiet_mode (! quiet_mode)
    2.11 +        (InductivePackage.add_inductive_global false big_rec_name false true false
    2.12             (map (fn s => (s, SOME UnivT', NoSyn)) rep_set_names') []
    2.13 -           (map (fn x => (("", []), x)) intr_ts) [] #>
    2.14 -         apsnd (ProofContext.theory_of o LocalTheory.exit)) thy1;
    2.15 +           (map (fn x => (("", []), x)) intr_ts) []) thy1;
    2.16  
    2.17      (********************************* typedef ********************************)
    2.18