internal inductive: fresh theorem group;
authorwenzelm
Sat Jan 26 17:08:35 2008 +0100 (2008-01-26)
changeset 25977b0604cd8e5e1
parent 25976 11c6811f232c
child 25978 8ba1eba8d058
internal inductive: fresh theorem group;
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/function_package/inductive_wrap.ML
src/HOL/Tools/inductive_realizer.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Fri Jan 25 23:50:33 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Sat Jan 26 17:08:35 2008 +0100
     1.3 @@ -564,6 +564,7 @@
     1.4      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
     1.5        setmp InductivePackage.quiet_mode false
     1.6          (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
     1.7 +            group = serial_string (),  (* FIXME pass proper group (!?) *)
     1.8              alt_name = big_rep_name, coind = false, no_elim = true, no_ind = false}
     1.9             (map (fn (s, T) => ((s, T --> HOLogic.boolT), NoSyn))
    1.10                (rep_set_names' ~~ recTs'))
    1.11 @@ -1488,6 +1489,7 @@
    1.12        thy10 |>
    1.13        setmp InductivePackage.quiet_mode (!quiet_mode)
    1.14          (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
    1.15 +            group = serial_string (),  (* FIXME pass proper group (!?) *)
    1.16              alt_name = big_rec_name, coind = false, no_elim = false, no_ind = false}
    1.17             (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    1.18             (map dest_Free rec_fns)
     2.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Jan 25 23:50:33 2008 +0100
     2.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sat Jan 26 17:08:35 2008 +0100
     2.3 @@ -156,6 +156,7 @@
     2.4      val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
     2.5        setmp InductivePackage.quiet_mode (!quiet_mode)
     2.6          (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
     2.7 +            group = serial_string (),  (* FIXME pass proper group (!?) *)
     2.8              alt_name = big_rec_name', coind = false, no_elim = false, no_ind = true}
     2.9             (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    2.10             (map dest_Free rec_fns)
     3.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Jan 25 23:50:33 2008 +0100
     3.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sat Jan 26 17:08:35 2008 +0100
     3.3 @@ -178,6 +178,7 @@
     3.4      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
     3.5        setmp InductivePackage.quiet_mode (! quiet_mode)
     3.6          (InductivePackage.add_inductive_global {verbose = false, kind = Thm.internalK,
     3.7 +            group = serial_string (),  (* FIXME pass proper group (!?) *)
     3.8              alt_name = big_rec_name, coind = false, no_elim = true, no_ind = false}
     3.9             (map (fn s => ((s, UnivT'), NoSyn)) rep_set_names') []
    3.10             (map (fn x => (("", []), x)) intr_ts) []) thy1;
     4.1 --- a/src/HOL/Tools/function_package/inductive_wrap.ML	Fri Jan 25 23:50:33 2008 +0100
     4.2 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Sat Jan 26 17:08:35 2008 +0100
     4.3 @@ -43,6 +43,7 @@
     4.4            InductivePackage.add_inductive_i
     4.5              {verbose = ! Toplevel.debug,
     4.6                kind = Thm.internalK,
     4.7 +              group = serial_string (),   (* FIXME pass proper group (!?) *)
     4.8                alt_name = "",
     4.9                coind = false,
    4.10                no_elim = false,
     5.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Jan 25 23:50:33 2008 +0100
     5.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Jan 26 17:08:35 2008 +0100
     5.3 @@ -351,6 +351,7 @@
     5.4  
     5.5      val (ind_info, thy3') = thy2 |>
     5.6        InductivePackage.add_inductive_global {verbose = false, kind = Thm.theoremK,
     5.7 +          group = serial_string (),  (* FIXME pass proper group (!?) *)
     5.8            alt_name = "", coind = false, no_elim = false, no_ind = false}
     5.9          rlzpreds rlzparams (map (fn (rintr, intr) =>
    5.10            ((Sign.base_name (name_of_thm intr), []),