--- 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 *)