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;