--- 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)