src/Pure/simplifier.ML
changeset 28863 32e83a854e5e
parent 28792 1d80cee865de
child 28965 1de908189869
     1.1 --- a/src/Pure/simplifier.ML	Thu Nov 20 14:55:28 2008 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Thu Nov 20 19:06:02 2008 +0100
     1.3 @@ -194,12 +194,12 @@
     1.4    in
     1.5      lthy |> LocalTheory.declaration (fn phi =>
     1.6        let
     1.7 -        val (naming', name) = Name.namify naming (Morphism.name phi (Name.binding name));
     1.8 +        val b' = Morphism.name phi (Name.binding name);
     1.9          val simproc' = morph_simproc phi simproc;
    1.10        in
    1.11          Simprocs.map (fn simprocs =>
    1.12 -            NameSpace.extend_table naming' [(name, simproc')] simprocs
    1.13 -              handle Symtab.DUP dup => err_dup_simproc dup)
    1.14 +          NameSpace.table_declare naming (b', simproc') simprocs |> snd
    1.15 +            handle Symtab.DUP dup => err_dup_simproc dup)
    1.16          #> map_ss (fn ss => ss addsimprocs [simproc'])
    1.17        end)
    1.18    end;