1.1 --- a/src/Pure/simplifier.ML	Tue Sep 02 12:07:34 2008 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Tue Sep 02 14:10:19 2008 +0200
     1.3 @@ -194,7 +194,7 @@
     1.4    in
     1.5      lthy |> LocalTheory.declaration (fn phi =>
     1.6        let
     1.7 -        val name' = Morphism.name phi name;
     1.8 +        val name' = Name.name_of (Morphism.name phi (Name.binding name));
     1.9          val simproc' = morph_simproc phi simproc;
    1.10        in
    1.11          Simprocs.map (fn simprocs =>