--- 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) [] ||>
--- 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;
--- 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;
--- 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 *)
--- 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)))
--- 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;