--- 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;
--- a/src/HOL/Tools/inductive_set_package.ML Fri Nov 14 08:50:08 2008 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML Fri Nov 14 08:50:09 2008 +0100
@@ -499,7 +499,7 @@
(* 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 *)
--- a/src/Pure/Isar/specification.ML Fri Nov 14 08:50:08 2008 +0100
+++ b/src/Pure/Isar/specification.ML Fri Nov 14 08:50:09 2008 +0100
@@ -345,7 +345,7 @@
lthy
|> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
|> (fn (res, lthy') =>
- if Name.name_of name = "" andalso null atts then
+ if Name.is_nothing name andalso null atts then
(ProofDisplay.print_results true lthy' ((kind, ""), res); lthy')
else
let