src/Pure/sign.ML
changeset 35200 aaddb2b526d6
parent 35129 ed24ba6f69aa
child 35255 2cb27605301f
equal deleted inserted replaced
35199:2e37cdae7b9c 35200:aaddb2b526d6
   125   val reset_group: theory -> theory
   125   val reset_group: theory -> theory
   126   val add_path: string -> theory -> theory
   126   val add_path: string -> theory -> theory
   127   val root_path: theory -> theory
   127   val root_path: theory -> theory
   128   val parent_path: theory -> theory
   128   val parent_path: theory -> theory
   129   val mandatory_path: string -> theory -> theory
   129   val mandatory_path: string -> theory -> theory
       
   130   val qualified_path: bool -> binding -> theory -> theory
   130   val local_path: theory -> theory
   131   val local_path: theory -> theory
   131   val restore_naming: theory -> theory -> theory
   132   val restore_naming: theory -> theory -> theory
   132   val hide_class: bool -> string -> theory -> theory
   133   val hide_class: bool -> string -> theory -> theory
   133   val hide_type: bool -> string -> theory -> theory
   134   val hide_type: bool -> string -> theory -> theory
   134   val hide_const: bool -> string -> theory -> theory
   135   val hide_const: bool -> string -> theory -> theory
   612 
   613 
   613 val add_path = map_naming o Name_Space.add_path;
   614 val add_path = map_naming o Name_Space.add_path;
   614 val root_path = map_naming Name_Space.root_path;
   615 val root_path = map_naming Name_Space.root_path;
   615 val parent_path = map_naming Name_Space.parent_path;
   616 val parent_path = map_naming Name_Space.parent_path;
   616 val mandatory_path = map_naming o Name_Space.mandatory_path;
   617 val mandatory_path = map_naming o Name_Space.mandatory_path;
       
   618 val qualified_path = map_naming oo Name_Space.qualified_path;
   617 
   619 
   618 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
   620 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
   619 
   621 
   620 val restore_naming = map_naming o K o naming_of;
   622 val restore_naming = map_naming o K o naming_of;
   621 
   623