src/Pure/General/name_space.ML
changeset 19305 5c16895d548b
parent 19055 4f408867f9d4
child 19367 6af9ee48b563
     1.1 --- a/src/Pure/General/name_space.ML	Tue Mar 21 12:18:13 2006 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Tue Mar 21 12:18:15 2006 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4  val is_hidden = String.isPrefix "??."
     1.5  
     1.6  val separator = ".";
     1.7 -val is_qualified = exists_string (equal separator);
     1.8 +val is_qualified = exists_string (fn s => s = separator);
     1.9  
    1.10  val pack = space_implode separator;
    1.11  val unpack = space_explode separator;
    1.12 @@ -229,7 +229,7 @@
    1.13      error ("Attempt to declare hidden name " ^ quote name)
    1.14    else
    1.15      let val names = unpack name in
    1.16 -      conditional (null names orelse exists (equal "") names) (fn () =>
    1.17 +      conditional (null names orelse exists (fn s => s = "") names) (fn () =>
    1.18          error ("Bad name declaration " ^ quote name));
    1.19        fold (add_name name) (map pack (accs names)) space
    1.20      end;