src/Pure/sign.ML

--- 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 "..";