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;