src/HOL/Nominal/nominal_package.ML
changeset 26536 e13479aa1d5d
parent 26475 3cc1e48d0ce1
child 26646 540ad65e804c
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Thu Apr 03 17:55:12 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Thu Apr 03 18:13:50 2008 +0200
     1.3 @@ -561,7 +561,8 @@
     1.4      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
     1.5          InductivePackage.add_inductive_global (serial_string ())
     1.6            {quiet_mode = false, verbose = false, kind = Thm.internalK,
     1.7 -            alt_name = big_rep_name, coind = false, no_elim = true, no_ind = false}
     1.8 +           alt_name = big_rep_name, coind = false, no_elim = true, no_ind = false,
     1.9 +           skip_mono = true}
    1.10            (map (fn (s, T) => ((s, T --> HOLogic.boolT), NoSyn))
    1.11               (rep_set_names' ~~ recTs'))
    1.12            [] (map (fn x => (("", []), x)) intr_ts) [] thy3;
    1.13 @@ -1484,7 +1485,8 @@
    1.14        thy10 |>
    1.15          InductivePackage.add_inductive_global (serial_string ())
    1.16            {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
    1.17 -            alt_name = big_rec_name, coind = false, no_elim = false, no_ind = false}
    1.18 +           alt_name = big_rec_name, coind = false, no_elim = false, no_ind = false,
    1.19 +           skip_mono = true}
    1.20            (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    1.21            (map dest_Free rec_fns)
    1.22            (map (fn x => (("", []), x)) rec_intr_ts) [] ||>