tuned -- Variable.declare_term is already part of Variable.auto_fixes;
authorwenzelm
Thu Nov 03 22:15:47 2011 +0100 (2011-11-03)
changeset 453268fa859aebc0d
parent 45325 26b6179b5a45
child 45327 4a027cc86f1a
tuned -- Variable.declare_term is already part of Variable.auto_fixes;
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/simplifier.ML	Thu Nov 03 11:18:06 2011 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Thu Nov 03 22:15:47 2011 +0100
     1.3 @@ -184,9 +184,7 @@
     1.4         lhss =
     1.5          let
     1.6            val lhss' = prep lthy lhss;
     1.7 -          val ctxt' = lthy
     1.8 -            |> fold Variable.declare_term lhss'
     1.9 -            |> fold Variable.auto_fixes lhss';
    1.10 +          val ctxt' = fold Variable.auto_fixes lhss' lthy;
    1.11          in Variable.export_terms ctxt' lthy lhss' end
    1.12          |> map (Thm.cterm_of (Proof_Context.theory_of lthy)),
    1.13         proc = proc,