src/HOL/Tools/inductive_set_package.ML

     local_theory -> InductivePackage.inductive_result * local_theory
   val add_inductive: bool -> bool ->
     (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;
 
 structure InductiveSetPackage: INDUCTIVE_SET_PACKAGE =

 fun code_ind_att optmod = to_pred_att [] #> InductiveCodegen.add optmod NONE;
 
 
 (**** 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;
     val {set_arities, pred_arities, to_pred_simps, ...} =
       PredSetConvData.get (Context.Proof ctxt);

     val cnames_syn' = map (fn (b, _) => (Binding.map_base (suffix "p") b, NoSyn)) cnames_syn;
     val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
     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 *)
     val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
       (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,

 local structure P = OuterParse and K = OuterKeyword in
 
 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;
 
 end;