# HG changeset patch
# User wenzelm
# Date 1231368788 -3600
# Node ID 0a49f940d72913fd482fe3dda3d36c5557951b93
# Parent  79eb3649ca9e470bbf0280d4f16bc8049e3dd63b
inductive: added fork_mono flag;

diff -r 79eb3649ca9e -r 0a49f940d729 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Wed Jan 07 23:52:18 2009 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Wed Jan 07 23:53:08 2009 +0100
@@ -571,7 +571,7 @@
         InductivePackage.add_inductive_global (serial_string ())
           {quiet_mode = false, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
-           skip_mono = true}
+           skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
              (rep_set_names' ~~ recTs'))
           [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy3;
@@ -1509,7 +1509,7 @@
         InductivePackage.add_inductive_global (serial_string ())
           {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
-           skip_mono = true}
+           skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
           (map dest_Free rec_fns)
           (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
diff -r 79eb3649ca9e -r 0a49f940d729 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Wed Jan 07 23:52:18 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Wed Jan 07 23:53:08 2009 +0100
@@ -155,7 +155,7 @@
         InductivePackage.add_inductive_global (serial_string ())
           {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
             alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
-            skip_mono = true}
+            skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
           (map dest_Free rec_fns)
           (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0;
diff -r 79eb3649ca9e -r 0a49f940d729 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Jan 07 23:52:18 2009 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Jan 07 23:53:08 2009 +0100
@@ -183,7 +183,7 @@
         InductivePackage.add_inductive_global (serial_string ())
           {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
-           skip_mono = true}
+           skip_mono = true, fork_mono = false}
           (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
           (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy1;
 
diff -r 79eb3649ca9e -r 0a49f940d729 src/HOL/Tools/function_package/inductive_wrap.ML
--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Wed Jan 07 23:52:18 2009 +0100
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Wed Jan 07 23:53:08 2009 +0100
@@ -48,7 +48,8 @@
               coind = false,
               no_elim = false,
               no_ind = false,
-              skip_mono = true}
+              skip_mono = true,
+              fork_mono = false}
             [((Binding.name R, T), NoSyn)] (* the relation *)
             [] (* no parameters *)
             (map (fn t => (Attrib.empty_binding, t)) defs) (* the intros *)
diff -r 79eb3649ca9e -r 0a49f940d729 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Jan 07 23:52:18 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Jan 07 23:53:08 2009 +0100
@@ -347,7 +347,7 @@
     val (ind_info, thy3') = thy2 |>
       InductivePackage.add_inductive_global (serial_string ())
         {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
-          coind = false, no_elim = false, no_ind = false, skip_mono = false}
+          coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
           ((Binding.name (Sign.base_name (name_of_thm intr)), []),
            subst_atomic rlzpreds' (Logic.unvarify rintr)))
diff -r 79eb3649ca9e -r 0a49f940d729 src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Wed Jan 07 23:52:18 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML	Wed Jan 07 23:53:08 2009 +0100
@@ -20,7 +20,7 @@
     (Binding.T * string option * mixfix) list ->
     (Binding.T * string option * mixfix) list ->
     (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
-    local_theory -> InductivePackage.inductive_result * local_theory
+    bool -> local_theory -> InductivePackage.inductive_result * local_theory
   val codegen_preproc: theory -> thm list -> thm list
   val setup: theory -> theory
 end;
@@ -403,7 +403,8 @@
 
 (**** definition of inductive sets ****)
 
-fun add_ind_set_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
+fun add_ind_set_def
+    {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
     cs intros monos params cnames_syn ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
@@ -468,7 +469,8 @@
     val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
       InductivePackage.add_ind_def
         {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Binding.empty,
-          coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
+          coind = coind, no_elim = no_elim, no_ind = no_ind,
+          skip_mono = skip_mono, fork_mono = fork_mono}
         cs' intros' monos' params1 cnames_syn' ctxt;
 
     (* define inductive sets using previously defined predicates *)
@@ -550,10 +552,10 @@
 val ind_set_decl = InductivePackage.gen_ind_decl add_ind_set_def;
 
 val _ =
-  OuterSyntax.local_theory "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
+  OuterSyntax.local_theory' "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
 
 val _ =
-  OuterSyntax.local_theory "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
+  OuterSyntax.local_theory' "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
 
 end;