# HG changeset patch
# User wenzelm
# Date 877601388 -7200
# Node ID 87941982f4754227faf66e41b7faf186f515d0ed
# Parent  b19d38604042b1c1b31ac3662a49fb576ef871f7
fixed prune of hidden short names;

diff -r b19d38604042 -r 87941982f475 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;