# HG changeset patch
# User haftmann
# Date 1227204362 -3600
# Node ID 32e83a854e5ee50e2bebf7265575bf1128e959a7
# Parent  53f13f763d4f06abac02a6e1b1092a4ad8b8ad8b
dropped legacy naming code

diff -r 53f13f763d4f -r 32e83a854e5e src/Pure/name.ML
--- a/src/Pure/name.ML	Thu Nov 20 14:55:28 2008 +0100
+++ b/src/Pure/name.ML	Thu Nov 20 19:06:02 2008 +0100
@@ -36,7 +36,6 @@
   val map_name: (string -> string) -> binding -> binding (*FIMXE legacy*)
   val qualified: string -> binding -> binding (*FIMXE legacy*)
   val display: binding -> string
-  val namify: NameSpace.naming -> binding -> NameSpace.naming * string (*FIMXE legacy*)
 end;
 
 structure Name: NAME =
@@ -167,14 +166,6 @@
     val pos = pos_of b;
   in f prefix (binding_pos (name, pos)) end;
 
-fun namify naming b =
-  let
-    val (prefix, name) = dest_binding b
-    fun mk_prefix (prfx, true) = sticky_prefix prfx
-      | mk_prefix (prfx, false) = add_path prfx;
-    val naming' = fold mk_prefix prefix naming;
-  in (naming', full naming' name) end;
-
 fun display b =
   let
     val (prefix, name) = dest_binding b
diff -r 53f13f763d4f -r 32e83a854e5e src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Nov 20 14:55:28 2008 +0100
+++ b/src/Pure/sign.ML	Thu Nov 20 19:06:02 2008 +0100
@@ -15,8 +15,6 @@
     consts: Consts.T}
   val naming_of: theory -> NameSpace.naming
   val base_name: string -> bstring
-  val name_decl: (string * 'a -> theory -> 'b * theory)
-    -> Name.binding * 'a -> theory -> (string * 'b) * theory
   val full_name: theory -> bstring -> string
   val full_binding: theory -> Name.binding -> string
   val full_name_path: theory -> string -> bstring -> string
@@ -191,19 +189,6 @@
 val naming_of = #naming o rep_sg;
 val base_name = NameSpace.base;
 
-fun name_decl decl (b, x) thy =
-  let
-    val naming = naming_of thy;
-    val (naming', name) = Name.namify naming b;
-  in
-    thy
-    |> map_naming (K naming')
-    |> decl (Name.name_of b, x)
-    |>> pair name
-    ||> map_naming (K naming)
-  end;
-
-val namify = Name.namify o naming_of;
 val full_name = NameSpace.full o naming_of;
 val full_binding = NameSpace.full_binding o naming_of;
 fun full_name_path thy elems = NameSpace.full (NameSpace.add_path elems (naming_of thy));
diff -r 53f13f763d4f -r 32e83a854e5e src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Nov 20 14:55:28 2008 +0100
+++ b/src/Pure/simplifier.ML	Thu Nov 20 19:06:02 2008 +0100
@@ -194,12 +194,12 @@
   in
     lthy |> LocalTheory.declaration (fn phi =>
       let
-        val (naming', name) = Name.namify naming (Morphism.name phi (Name.binding name));
+        val b' = Morphism.name phi (Name.binding name);
         val simproc' = morph_simproc phi simproc;
       in
         Simprocs.map (fn simprocs =>
-            NameSpace.extend_table naming' [(name, simproc')] simprocs
-              handle Symtab.DUP dup => err_dup_simproc dup)
+          NameSpace.table_declare naming (b', simproc') simprocs |> snd
+            handle Symtab.DUP dup => err_dup_simproc dup)
         #> map_ss (fn ss => ss addsimprocs [simproc'])
       end)
   end;