fixed prune of hidden short names;
authorwenzelm
Thu, 23 Oct 1997 12:09:48 +0200
changeset 3972 87941982f475
parent 3971 b19d38604042
child 3973 1be726ef6813
fixed prune of hidden short names;
src/Pure/name_space.ML
--- a/src/Pure/name_space.ML	Thu Oct 23 12:09:31 1997 +0200
+++ b/src/Pure/name_space.ML	Thu Oct 23 12:09:48 1997 +0200
@@ -98,14 +98,12 @@
   if_none (Symtab.lookup (tab_of space, name)) name;
 
 fun prune space name =
-  if not (qualified name) then name
-  else
-    let
-      fun try [] = "??" ^ separator ^ name      (*hidden name*)
-        | try (nm :: nms) =
-            if lookup space nm = name then nm
-            else try nms;
-    in try (map pack (suffixes1 (unpack name))) end;
+  let
+    fun try [] = "??" ^ separator ^ name      (*hidden name*)
+      | try (nm :: nms) =
+          if lookup space nm = name then nm
+          else try nms;
+  in try (map pack (suffixes1 (unpack name))) end;
 
 
 end;