# HG changeset patch
# User wenzelm
# Date 894794371 -7200
# Node ID 7a155899ef9c151749c7d66c3b6554d830e9ccfe
# Parent  0eb6730de30f0866d30d8ea4d9a7a5dc533f3251
tuned comment;

diff -r 0eb6730de30f -r 7a155899ef9c src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri May 08 18:33:29 1998 +0200
+++ b/src/Pure/sign.ML	Sun May 10 11:59:31 1998 +0200
@@ -455,7 +455,7 @@
   val intern_tycons = intrn_tycons o spaces_of;
 
   val full_name = full o #path o rep_sg;
-  fun full_name_path sg elems name =		(* FIXME "..", "/" semantics (!?) *)
+  fun full_name_path sg elems name =
     full (#path (rep_sg sg) @ NameSpace.unpack elems) name;
 end;