src/HOL/Tools/inductive_set.ML

         Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
       else alt_name;
     val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn;  (* FIXME *)
     val (intr_names, intr_atts) = split_list (map fst intros);
     val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
-    val (intrs', elims', induct, lthy4) =
+    val (intrs', elims', induct, inducts, lthy4) =
       Inductive.declare_rules rec_name coind no_ind cnames
         (map (to_set [] (Context.Proof lthy3)) intrs) intr_names intr_atts
         (map (fn th => (to_set [] (Context.Proof lthy3) th,
            map fst (fst (Rule_Cases.get th)),
            Rule_Cases.get_constraints th)) elims)
         raw_induct' lthy3;
   in
-    ({intrs = intrs', elims = elims', induct = induct,
+    ({intrs = intrs', elims = elims', induct = induct, inducts = inducts,
       raw_induct = raw_induct', preds = map fst defs},
      lthy4)
   end;
 
 val add_inductive_i = Inductive.gen_add_inductive_i add_ind_set_def;