# HG changeset patch
# User wenzelm
# Date 1320354947 -3600
# Node ID 8fa859aebc0dc3fea4f771d669f03b005c2a4797
# Parent  26b6179b5a450783b7444cc299b26319a481a139
tuned -- Variable.declare_term is already part of Variable.auto_fixes;

diff -r 26b6179b5a45 -r 8fa859aebc0d src/Pure/simplifier.ML
--- 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,