src/Pure/General/name_space.ML
changeset 21962 279b129498b6
parent 21914 77372f38aa98
child 22057 d7c91b2f5a9e
     1.1 --- a/src/Pure/General/name_space.ML	Sat Dec 30 12:41:59 2006 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Sat Dec 30 16:08:00 2006 +0100
     1.3 @@ -232,11 +232,11 @@
     1.4    if is_hidden name then
     1.5      error ("Attempt to declare hidden name " ^ quote name)
     1.6    else
     1.7 -    let val names = explode_name name in
     1.8 -      conditional (null names orelse exists (fn s => s = "") names) (fn () =>
     1.9 -        error ("Bad name declaration " ^ quote name));
    1.10 -      fold (add_name name) (map implode_name (accs names)) space
    1.11 -    end;
    1.12 +    let
    1.13 +      val names = explode_name name;
    1.14 +      val _ = (null names orelse exists (fn s => s = "") names) andalso
    1.15 +        error ("Bad name declaration " ^ quote name);
    1.16 +    in fold (add_name name) (map implode_name (accs names)) space end;
    1.17  
    1.18  
    1.19  (* manipulate namings *)