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;