src/HOL/Tools/inductive_set_package.ML
changeset 29389 0a49f940d729
parent 29288 253bcf2a5854
child 29581 b3b33e0298eb
     1.1 --- a/src/HOL/Tools/inductive_set_package.ML	Wed Jan 07 23:52:18 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Wed Jan 07 23:53:08 2009 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4      (Binding.T * string option * mixfix) list ->
     1.5      (Binding.T * string option * mixfix) list ->
     1.6      (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
     1.7 -    local_theory -> InductivePackage.inductive_result * local_theory
     1.8 +    bool -> local_theory -> InductivePackage.inductive_result * local_theory
     1.9    val codegen_preproc: theory -> thm list -> thm list
    1.10    val setup: theory -> theory
    1.11  end;
    1.12 @@ -403,7 +403,8 @@
    1.13  
    1.14  (**** definition of inductive sets ****)
    1.15  
    1.16 -fun add_ind_set_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
    1.17 +fun add_ind_set_def
    1.18 +    {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
    1.19      cs intros monos params cnames_syn ctxt =
    1.20    let
    1.21      val thy = ProofContext.theory_of ctxt;
    1.22 @@ -468,7 +469,8 @@
    1.23      val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
    1.24        InductivePackage.add_ind_def
    1.25          {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Binding.empty,
    1.26 -          coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
    1.27 +          coind = coind, no_elim = no_elim, no_ind = no_ind,
    1.28 +          skip_mono = skip_mono, fork_mono = fork_mono}
    1.29          cs' intros' monos' params1 cnames_syn' ctxt;
    1.30  
    1.31      (* define inductive sets using previously defined predicates *)
    1.32 @@ -550,10 +552,10 @@
    1.33  val ind_set_decl = InductivePackage.gen_ind_decl add_ind_set_def;
    1.34  
    1.35  val _ =
    1.36 -  OuterSyntax.local_theory "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
    1.37 +  OuterSyntax.local_theory' "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false);
    1.38  
    1.39  val _ =
    1.40 -  OuterSyntax.local_theory "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
    1.41 +  OuterSyntax.local_theory' "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true);
    1.42  
    1.43  end;
    1.44