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

diff -r a2cb4de2a1aa -r 66bca8a4079c src/HOL/Tools/function_package/inductive_wrap.ML
--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Thu Apr 03 17:54:19 2008 +0200
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Thu Apr 03 17:55:12 2008 +0200
@@ -47,7 +47,8 @@
               alt_name = "",
               coind = false,
               no_elim = false,
-              no_ind = false}
+              no_ind = false,
+              skip_mono = true}
             [((R, T), NoSyn)] (* the relation *)
             [] (* no parameters *)
             (map (fn t => (("", []), t)) defs) (* the intros *)
diff -r a2cb4de2a1aa -r 66bca8a4079c src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Apr 03 17:54:19 2008 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Apr 03 17:55:12 2008 +0200
@@ -351,7 +351,7 @@
     val (ind_info, thy3') = thy2 |>
       InductivePackage.add_inductive_global (serial_string ())
         {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = "",
-          coind = false, no_elim = false, no_ind = false}
+          coind = false, no_elim = false, no_ind = false, skip_mono = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
           ((Sign.base_name (name_of_thm intr), []),
            subst_atomic rlzpreds' (Logic.unvarify rintr)))