# HG changeset patch
# User wenzelm
# Date 1257863563 -3600
# Node ID c40ced05b10ab4873f581623e0adcddbfac874ad
# Parent  4e1708efa79e1b9f3b9cfde9d51fd75dc831f093
define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;

diff -r 4e1708efa79e -r c40ced05b10a src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Tue Nov 10 14:38:39 2009 +0100
+++ b/src/Pure/simplifier.ML	Tue Nov 10 15:32:43 2009 +0100
@@ -189,8 +189,7 @@
         in Variable.export_terms ctxt' lthy lhss' end
         |> map (Thm.cterm_of (ProofContext.theory_of lthy)),
        proc = proc,
-       identifier = identifier}
-      |> morph_simproc (LocalTheory.target_morphism lthy);
+       identifier = identifier};
   in
     lthy |> LocalTheory.declaration false (fn phi =>
       let