# HG changeset patch
# User haftmann
# Date 1226649009 -3600
# Node ID cc16be808796424cc1698c0d56bf3aeb63e1e5b5
# Parent  2efba7b18c5b28d29913bce7d72f392795bcfe2d
Name.is_nothing

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;
 
diff -r 2efba7b18c5b -r cc16be808796 src/HOL/Tools/inductive_set_package.ML
--- 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 *)
diff -r 2efba7b18c5b -r cc16be808796 src/Pure/Isar/specification.ML
--- 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