--- a/src/Pure/General/name_space.ML Sat Dec 30 12:41:59 2006 +0100
+++ b/src/Pure/General/name_space.ML Sat Dec 30 16:08:00 2006 +0100
@@ -232,11 +232,11 @@
if is_hidden name then
error ("Attempt to declare hidden name " ^ quote name)
else
- let val names = explode_name name in
- conditional (null names orelse exists (fn s => s = "") names) (fn () =>
- error ("Bad name declaration " ^ quote name));
- fold (add_name name) (map implode_name (accs names)) space
- end;
+ let
+ val names = explode_name name;
+ val _ = (null names orelse exists (fn s => s = "") names) andalso
+ error ("Bad name declaration " ^ quote name);
+ in fold (add_name name) (map implode_name (accs names)) space end;
(* manipulate namings *)