src/HOL/Tools/inductive_package.ML

        else foldr1 HOLogic.mk_disj (map transform_rule intr_ts));
 
     (* add definiton of recursive predicates to theory *)
 
     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 ((rec_const, (_, fp_def)), ctxt') = ctxt |>
       LocalTheory.define Thm.internalK