src/HOL/Tools/inductive_set_package.ML

 sig
   val to_set_att: thm list -> attribute
   val to_pred_att: thm list -> attribute
   val pred_set_conv_att: attribute
   val add_inductive_i:
-    {verbose: bool, kind: string, group: string, alt_name: bstring,
-      coind: bool, no_elim: bool, no_ind: bool} ->
+    {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
     ((string * typ) * mixfix) list ->
     (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
       local_theory -> InductivePackage.inductive_result * local_theory
   val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
     (string * string option * mixfix) list ->

 fun code_ind_att optmod = to_pred_att [] #> InductiveCodegen.add optmod NONE;
 
 
 (**** definition of inductive sets ****)
 
-fun add_ind_set_def {verbose, kind, group, alt_name, coind, no_elim, no_ind}
+fun add_ind_set_def {verbose, kind, alt_name, coind, no_elim, no_ind}
     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);

         Pattern.rewrite_term thy [] [to_pred_proc thy eqns'] |>
         eta_contract (member op = cs' orf is_pred pred_arities))) intros;
     val cnames_syn' = map (fn (s, _) => (s ^ "p", NoSyn)) cnames_syn;
     val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
     val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
-      InductivePackage.add_ind_def {verbose = verbose, kind = kind, group = group,
-          alt_name = "",  (* FIXME pass alt_name (!?) *)
+      InductivePackage.add_ind_def {verbose = verbose, kind = kind, alt_name = "",
           coind = coind, no_elim = no_elim, no_ind = no_ind}
         cs' intros' monos' params1 cnames_syn' ctxt;
 
     (* define inductive sets using previously defined predicates *)
     val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)

       space_implode "_" (map fst cnames_syn) else alt_name;
     val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o #1) cnames_syn;  (* FIXME *)
     val (intr_names, intr_atts) = split_list (map fst intros);
     val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
     val (intrs', elims', induct, ctxt4) =
-      InductivePackage.declare_rules kind group rec_name coind no_ind cnames
+      InductivePackage.declare_rules kind rec_name coind no_ind cnames
       (map (to_set [] (Context.Proof ctxt3)) intrs) intr_names intr_atts
       (map (fn th => (to_set [] (Context.Proof ctxt3) th,
          map fst (fst (RuleCases.get th)))) elims)
       raw_induct' ctxt3
   in