--- a/src/Pure/sign.ML Sun Oct 25 19:14:46 2009 +0100
+++ b/src/Pure/sign.ML Sun Oct 25 19:17:42 2009 +0100
@@ -12,6 +12,7 @@
syn: Syntax.syntax,
tsig: Type.tsig,
consts: Consts.T}
+ val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory
val naming_of: theory -> Name_Space.naming
val full_name: theory -> binding -> string
val full_name_path: theory -> string -> binding -> string
@@ -125,7 +126,6 @@
val parent_path: theory -> theory
val mandatory_path: string -> theory -> theory
val local_path: theory -> theory
- val conceal: theory -> theory
val restore_naming: theory -> theory -> theory
val hide_class: bool -> string -> theory -> theory
val hide_type: bool -> string -> theory -> theory
@@ -619,8 +619,6 @@
fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
-val conceal = map_naming Name_Space.conceal;
-
val restore_naming = map_naming o K o naming_of;