diff -r d743bb1b6c23 -r 89d19aa73081 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Sun Apr 17 22:10:09 2016 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Sun Apr 17 22:38:50 2016 +0200
@@ -495,9 +495,7 @@
 
     (* convert theorems to set notation *)
     val rec_name =
-      if Binding.is_empty alt_name then
-        Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
-      else alt_name;
+      if Binding.is_empty alt_name then Binding.conglomerate (map #1 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;