# HG changeset patch
# User wenzelm
# Date 1236716401 -3600
# Node ID 9498e99e58a66f6a6aa6594d2f5e1c2f6ef474eb
# Parent  ebbec8d8d7a9aa2b89bc23f70fac2198507b74a2
explicit root_path, parent_path;
derived absolute_path;
tuned;

diff -r ebbec8d8d7a9 -r 9498e99e58a6 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Mar 10 21:19:22 2009 +0100
+++ b/src/Pure/sign.ML	Tue Mar 10 21:20:01 2009 +0100
@@ -122,13 +122,13 @@
   val add_trrules_i: ast Syntax.trrule list -> theory -> theory
   val del_trrules_i: ast Syntax.trrule list -> theory -> theory
   val add_path: string -> theory -> theory
+  val root_path: theory -> theory
   val parent_path: theory -> theory
-  val root_path: theory -> theory
+  val sticky_prefix: string -> theory -> theory
+  val no_base_names: theory -> theory
+  val qualified_names: theory -> theory
   val absolute_path: theory -> theory
   val local_path: theory -> theory
-  val no_base_names: theory -> theory
-  val qualified_names: theory -> theory
-  val sticky_prefix: string -> theory -> theory
   val restore_naming: theory -> theory -> theory
   val hide_class: bool -> string -> theory -> theory
   val hide_type: bool -> string -> theory -> theory
@@ -619,17 +619,18 @@
 (* naming *)
 
 val add_path        = map_naming o NameSpace.add_path;
+val root_path       = map_naming NameSpace.root_path;
+val parent_path     = map_naming NameSpace.parent_path;
+val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
 val no_base_names   = map_naming NameSpace.no_base_names;
 val qualified_names = map_naming NameSpace.qualified_names;
-val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
-val restore_naming  = map_naming o K o naming_of;
 
-val parent_path   = add_path "..";
-val root_path     = add_path "/";
-val absolute_path = add_path "//";
+val absolute_path = root_path o qualified_names;
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
 
+val restore_naming  = map_naming o K o naming_of;
+
 
 (* hide names *)