src/Pure/sign.ML
changeset 30522 e26b80647189
parent 30469 de9e8f1d927c
child 30585 6b2ba4666336
     1.1 --- a/src/Pure/sign.ML	Fri Mar 13 23:56:07 2009 +0100
     1.2 +++ b/src/Pure/sign.ML	Sat Mar 14 00:13:50 2009 +0100
     1.3 @@ -125,7 +125,6 @@
     1.4    val root_path: theory -> theory
     1.5    val parent_path: theory -> theory
     1.6    val mandatory_path: string -> theory -> theory
     1.7 -  val no_base_names: 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 @@ -616,15 +615,14 @@
    1.12  
    1.13  (* naming *)
    1.14  
    1.15 -val add_path        = map_naming o NameSpace.add_path;
    1.16 -val root_path       = map_naming NameSpace.root_path;
    1.17 -val parent_path     = map_naming NameSpace.parent_path;
    1.18 -val mandatory_path  = map_naming o NameSpace.mandatory_path;
    1.19 -val no_base_names   = map_naming NameSpace.no_base_names;
    1.20 +val add_path = map_naming o NameSpace.add_path;
    1.21 +val root_path = map_naming NameSpace.root_path;
    1.22 +val parent_path = map_naming NameSpace.parent_path;
    1.23 +val mandatory_path = map_naming o NameSpace.mandatory_path;
    1.24  
    1.25  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
    1.26  
    1.27 -val restore_naming  = map_naming o K o naming_of;
    1.28 +val restore_naming = map_naming o K o naming_of;
    1.29  
    1.30  
    1.31  (* hide names *)