src/HOL/Tools/inductive_package.ML
changeset 28791 cc16be808796
parent 28524 644b62cf678f
child 28839 32d498cf7595
--- 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;