Name.is_nothing
authorhaftmann
Fri Nov 14 08:50:09 2008 +0100 (2008-11-14)
changeset 28791cc16be808796
parent 28790 2efba7b18c5b
child 28792 1d80cee865de
Name.is_nothing
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_set_package.ML
src/Pure/Isar/specification.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Nov 14 08:50:08 2008 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Nov 14 08:50:09 2008 +0100
     1.3 @@ -638,7 +638,7 @@
     1.4      (* add definiton of recursive predicates to theory *)
     1.5  
     1.6      val rec_name =
     1.7 -      if Name.name_of alt_name = "" then
     1.8 +      if Name.is_nothing alt_name then
     1.9          Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
    1.10        else alt_name;
    1.11  
     2.1 --- a/src/HOL/Tools/inductive_set_package.ML	Fri Nov 14 08:50:08 2008 +0100
     2.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Fri Nov 14 08:50:09 2008 +0100
     2.3 @@ -499,7 +499,7 @@
     2.4  
     2.5      (* convert theorems to set notation *)
     2.6      val rec_name =
     2.7 -      if Name.name_of alt_name = "" then
     2.8 +      if Name.is_nothing alt_name then
     2.9          Name.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
    2.10        else alt_name;
    2.11      val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn;  (* FIXME *)
     3.1 --- a/src/Pure/Isar/specification.ML	Fri Nov 14 08:50:08 2008 +0100
     3.2 +++ b/src/Pure/Isar/specification.ML	Fri Nov 14 08:50:09 2008 +0100
     3.3 @@ -345,7 +345,7 @@
     3.4          lthy
     3.5          |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
     3.6          |> (fn (res, lthy') =>
     3.7 -          if Name.name_of name = "" andalso null atts then
     3.8 +          if Name.is_nothing name andalso null atts then
     3.9              (ProofDisplay.print_results true lthy' ((kind, ""), res); lthy')
    3.10            else
    3.11              let