src/Pure/simplifier.ML
changeset 28965 1de908189869
parent 28863 32e83a854e5e
child 28991 694227dd3e8c
     1.1 --- a/src/Pure/simplifier.ML	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/Pure/simplifier.ML	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -194,11 +194,11 @@
     1.4    in
     1.5      lthy |> LocalTheory.declaration (fn phi =>
     1.6        let
     1.7 -        val b' = Morphism.name phi (Name.binding name);
     1.8 +        val b' = Morphism.binding phi (Binding.name name);
     1.9          val simproc' = morph_simproc phi simproc;
    1.10        in
    1.11          Simprocs.map (fn simprocs =>
    1.12 -          NameSpace.table_declare naming (b', simproc') simprocs |> snd
    1.13 +          NameSpace.bind naming (b', simproc') simprocs |> snd
    1.14              handle Symtab.DUP dup => err_dup_simproc dup)
    1.15          #> map_ss (fn ss => ss addsimprocs [simproc'])
    1.16        end)