--- a/src/Pure/sign.ML Wed Oct 17 23:16:28 2007 +0200
+++ b/src/Pure/sign.ML Wed Oct 17 23:16:30 2007 +0200
@@ -53,8 +53,6 @@
val no_base_names: theory -> theory
val qualified_names: theory -> theory
val sticky_prefix: string -> theory -> theory
- val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
- theory -> theory
val restore_naming: theory -> theory -> theory
end
@@ -785,7 +783,6 @@
val no_base_names = map_naming NameSpace.no_base_names;
val qualified_names = map_naming NameSpace.qualified_names;
val sticky_prefix = map_naming o NameSpace.sticky_prefix;
-val set_policy = map_naming o NameSpace.set_policy;
val restore_naming = map_naming o K o naming_of;
val parent_path = add_path "..";