src/HOL/Tools/inductive.ML

   type add_ind_def =
     flags ->
     term list -> (Attrib.binding * term) list -> thm list ->
     term list -> (binding * mixfix) list ->
     local_theory -> result * local_theory
-  val declare_rules: binding -> bool -> bool -> string -> string list -> term list ->
+  val declare_rules: binding -> bool -> bool -> binding -> string list -> term list ->
     thm list -> binding list -> Token.src list list -> (thm * string list * int) list ->
     thm list -> thm -> local_theory -> thm list * thm list * thm list * thm * thm list * local_theory
   val add_ind_def: add_ind_def
   val gen_add_inductive: add_ind_def -> flags ->
     ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->

     val _ = null cnames_syn andalso error "No inductive predicates given";
     val names = map (Binding.name_of o fst) cnames_syn;
     val _ = message (quiet_mode andalso not verbose)
       ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
 
-    val spec_name = Local_Theory.full_name lthy (Binding.conglomerate (map #1 cnames_syn));
+    val spec_name = Binding.conglomerate (map #1 cnames_syn);
     val cnames = map (Local_Theory.full_name lthy o #1) cnames_syn;  (* FIXME *)
     val ((intr_names, intr_atts), intr_ts) =
       apfst split_list (split_list (map (check_rule lthy cs params) intros));
 
     val (lthy1, lthy2, rec_binding, mono, fp_def, rec_preds_defs, rec_const, preds,