Drop illegitimate optimisation from d5a7f2c54655.
authorballarin
Fri Mar 02 15:14:59 2018 +0100 (2018-03-02)
changeset 677426306bd582957
parent 67741 d5a7f2c54655
child 67747 7b84ecd54d70
Drop illegitimate optimisation from d5a7f2c54655.
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Mar 02 14:28:39 2018 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Mar 02 15:14:59 2018 +0100
     1.3 @@ -407,8 +407,7 @@
     1.4            |> Variable.export_terms ctxt' ctxt
     1.5            |> Element.eq_term_morphism (Proof_Context.theory_of ctxt)
     1.6            |> the_default Morphism.identity;
     1.7 -       val ctxt'' = if null eqns then ctxt' else 
     1.8 -         Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
     1.9 +       val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
    1.10         val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns'];
    1.11        in (i + 1, insts', eqnss', ctxt'') end;
    1.12