define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;

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