--- 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;