diff -r f6d9e0e0b153 -r 1de908189869 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Dec 03 21:00:39 2008 -0800
+++ b/src/Pure/simplifier.ML	Thu Dec 04 14:43:33 2008 +0100
@@ -194,11 +194,11 @@
   in
     lthy |> LocalTheory.declaration (fn phi =>
       let
-        val b' = Morphism.name phi (Name.binding name);
+        val b' = Morphism.binding phi (Binding.name name);
         val simproc' = morph_simproc phi simproc;
       in
         Simprocs.map (fn simprocs =>
-          NameSpace.table_declare naming (b', simproc') simprocs |> snd
+          NameSpace.bind naming (b', simproc') simprocs |> snd
             handle Symtab.DUP dup => err_dup_simproc dup)
         #> map_ss (fn ss => ss addsimprocs [simproc'])
       end)