# HG changeset patch
# User berghofe
# Date 1207239230 -7200
# Node ID e13479aa1d5d4960663f6295d3a34c6fcc47525b
# Parent  66bca8a4079ccf5832fd2ae63a506440a9913c78
Added skip_mono flag to inductive definition package.

diff -r 66bca8a4079c -r e13479aa1d5d src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Thu Apr 03 17:55:12 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Thu Apr 03 18:13:50 2008 +0200
@@ -561,7 +561,8 @@
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
         InductivePackage.add_inductive_global (serial_string ())
           {quiet_mode = false, verbose = false, kind = Thm.internalK,
-            alt_name = big_rep_name, coind = false, no_elim = true, no_ind = false}
+           alt_name = big_rep_name, coind = false, no_elim = true, no_ind = false,
+           skip_mono = true}
           (map (fn (s, T) => ((s, T --> HOLogic.boolT), NoSyn))
              (rep_set_names' ~~ recTs'))
           [] (map (fn x => (("", []), x)) intr_ts) [] thy3;
@@ -1484,7 +1485,8 @@
       thy10 |>
         InductivePackage.add_inductive_global (serial_string ())
           {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
-            alt_name = big_rec_name, coind = false, no_elim = false, no_ind = false}
+           alt_name = big_rec_name, coind = false, no_elim = false, no_ind = false,
+           skip_mono = true}
           (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
           (map dest_Free rec_fns)
           (map (fn x => (("", []), x)) rec_intr_ts) [] ||>