# HG changeset patch
# User wenzelm
# Date 1117729789 -7200
# Node ID 74dc76a28038cc1b9852c811ae1a69f9cb4d7b03
# Parent  841342a7c41c7ff14b7b5929b981f7bf846d8828
replaced set_naming by restore_naming;

diff -r 841342a7c41c -r 74dc76a28038 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Jun 02 18:29:48 2005 +0200
+++ b/src/Pure/sign.ML	Thu Jun 02 18:29:49 2005 +0200
@@ -158,7 +158,7 @@
   val no_base_names: sg -> sg
   val custom_accesses: (string list -> string list list) -> sg -> sg
   val set_policy: (string -> bstring -> string) * (string list -> string list list) -> sg -> sg
-  val set_naming: NameSpace.naming -> sg -> sg
+  val restore_naming: sg -> sg -> sg
   val add_space: string * string list -> sg -> sg
   val hide_space: bool -> string * string list -> sg -> sg
   val hide_space_i: bool -> string * string list -> sg -> sg
@@ -1118,7 +1118,7 @@
 val no_base_names        = extend_sign true (change_naming (K NameSpace.no_base_names)) "#" ();
 val custom_accesses      = extend_sign true (change_naming NameSpace.custom_accesses) "#";
 val set_policy           = extend_sign true (change_naming NameSpace.set_policy) "#";
-val set_naming           = extend_sign true (change_naming K) "#";
+val restore_naming       = extend_sign true (change_naming (K o naming_of)) "#";
 val add_space            = extend_sign true ext_add_space "#";
 val hide_space           = curry (extend_sign true ext_hide_space "#");
 val hide_space_i         = curry (extend_sign true ext_hide_space_i "#");