tuned -- Variable.declare_term is already part of Variable.auto_fixes;

--- a/src/Pure/simplifier.ML	Thu Nov 03 11:18:06 2011 +0100
+++ b/src/Pure/simplifier.ML	Thu Nov 03 22:15:47 2011 +0100
@@ -184,9 +184,7 @@
        lhss =
         let
           val lhss' = prep lthy lhss;
-          val ctxt' = lthy
-            |> fold Variable.declare_term lhss'
-            |> fold Variable.auto_fixes lhss';
+          val ctxt' = fold Variable.auto_fixes lhss' lthy;
         in Variable.export_terms ctxt' lthy lhss' end
         |> map (Thm.cterm_of (Proof_Context.theory_of lthy)),
        proc = proc,