src/Pure/sign.ML
changeset 30436 0e3c88f132fc
parent 30421 9498e99e58a6
child 30438 c2d49315b93b
     1.1 --- a/src/Pure/sign.ML	Wed Mar 11 15:42:19 2009 +0100
     1.2 +++ b/src/Pure/sign.ML	Wed Mar 11 15:44:12 2009 +0100
     1.3 @@ -127,7 +127,6 @@
     1.4    val sticky_prefix: string -> theory -> theory
     1.5    val no_base_names: theory -> theory
     1.6    val qualified_names: theory -> theory
     1.7 -  val absolute_path: theory -> theory
     1.8    val local_path: theory -> theory
     1.9    val restore_naming: theory -> theory -> theory
    1.10    val hide_class: bool -> string -> theory -> theory
    1.11 @@ -625,8 +624,6 @@
    1.12  val no_base_names   = map_naming NameSpace.no_base_names;
    1.13  val qualified_names = map_naming NameSpace.qualified_names;
    1.14  
    1.15 -val absolute_path = root_path o qualified_names;
    1.16 -
    1.17  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
    1.18  
    1.19  val restore_naming  = map_naming o K o naming_of;