normalize proof before splitting conjunctions, according to Proof.conclude_goal (see also 4dd0ba632e40) -- may reduce general resource usage;
authorwenzelm
Tue Jul 14 11:29:43 2015 +0200 (2015-07-14)
changeset 60722a8babbb6d5ea
parent 60719 b6713e04889e
child 60723 757cad5a3fe9
normalize proof before splitting conjunctions, according to Proof.conclude_goal (see also 4dd0ba632e40) -- may reduce general resource usage;
src/Pure/goal.ML
     1.1 --- a/src/Pure/goal.ML	Mon Jul 13 19:25:58 2015 +0200
     1.2 +++ b/src/Pure/goal.ML	Tue Jul 14 11:29:43 2015 +0200
     1.3 @@ -230,7 +230,9 @@
     1.4              result)
     1.5            (Thm.term_of stmt);
     1.6    in
     1.7 -    Conjunction.elim_balanced (length props) res
     1.8 +    res
     1.9 +    |> length props > 1 ? Thm.norm_proof
    1.10 +    |> Conjunction.elim_balanced (length props)
    1.11      |> map (Assumption.export false ctxt' ctxt)
    1.12      |> Variable.export ctxt' ctxt
    1.13      |> map Drule.zero_var_indexes