# HG changeset patch
# User wenzelm
# Date 1236782652 -3600
# Node ID 0e3c88f132fc63fcbe0164334b616fb5797f6786
# Parent  e62d6ecab6ad717476d380237bc5fcbad54bf236
removed obsolete absolute_path -- use root_path with qualified binding;

diff -r e62d6ecab6ad -r 0e3c88f132fc src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Mar 11 15:42:19 2009 +0100
+++ b/src/Pure/sign.ML	Wed Mar 11 15:44:12 2009 +0100
@@ -127,7 +127,6 @@
   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 restore_naming: theory -> theory -> theory
   val hide_class: bool -> string -> theory -> theory
@@ -625,8 +624,6 @@
 val no_base_names   = map_naming NameSpace.no_base_names;
 val qualified_names = map_naming NameSpace.qualified_names;
 
-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;