# HG changeset patch
# User wenzelm
# Date 1192655790 -7200
# Node ID 6680bebdfc2814d9c64234a63e6b9e1cd29c6a50
# Parent  e2a39b6526b0f28245e15ec3edf78b21740379ed
removed unused set_policy;

diff -r e2a39b6526b0 -r 6680bebdfc28 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 "..";