removed obsolete absolute_path -- use root_path with qualified binding;
authorwenzelm
Wed, 11 Mar 2009 15:44:12 +0100
changeset 30436 0e3c88f132fc
parent 30435 e62d6ecab6ad
child 30437 910a7aeb8dec
removed obsolete absolute_path -- use root_path with qualified binding;
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;