diff -r 2efba7b18c5b -r cc16be808796 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Nov 14 08:50:08 2008 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Nov 14 08:50:09 2008 +0100
@@ -638,7 +638,7 @@
     (* 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;