removed unused set_policy;
authorwenzelm
Wed Oct 17 23:16:30 2007 +0200 (2007-10-17)
changeset 250716680bebdfc28
parent 25070 e2a39b6526b0
child 25072 03f57b516e12
removed unused set_policy;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Wed Oct 17 23:16:28 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Wed Oct 17 23:16:30 2007 +0200
     1.3 @@ -53,8 +53,6 @@
     1.4    val no_base_names: theory -> theory
     1.5    val qualified_names: theory -> theory
     1.6    val sticky_prefix: string -> theory -> theory
     1.7 -  val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
     1.8 -    theory -> theory
     1.9    val restore_naming: theory -> theory -> theory
    1.10  end
    1.11  
    1.12 @@ -785,7 +783,6 @@
    1.13  val no_base_names   = map_naming NameSpace.no_base_names;
    1.14  val qualified_names = map_naming NameSpace.qualified_names;
    1.15  val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
    1.16 -val set_policy      = map_naming o NameSpace.set_policy;
    1.17  val restore_naming  = map_naming o K o naming_of;
    1.18  
    1.19  val parent_path   = add_path "..";