src/HOL/Tools/inductive_set_package.ML

               [conv_thm]) |> snd
         end) (preds ~~ cs ~~ cs_info ~~ defs) ctxt2;
 
     (* convert theorems to set notation *)
     val rec_name =
-      if Name.name_of alt_name = "" then
+      if Name.is_nothing alt_name then
         Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
       else alt_name;
     val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o Name.name_of 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;