changeset 60722 | a8babbb6d5ea |
parent 60695 | 757549b4bbe6 |
child 60723 | 757cad5a3fe9 |
--- a/src/Pure/goal.ML Mon Jul 13 19:25:58 2015 +0200 +++ b/src/Pure/goal.ML Tue Jul 14 11:29:43 2015 +0200 @@ -230,7 +230,9 @@ result) (Thm.term_of stmt); in - Conjunction.elim_balanced (length props) res + res + |> length props > 1 ? Thm.norm_proof + |> Conjunction.elim_balanced (length props) |> map (Assumption.export false ctxt' ctxt) |> Variable.export ctxt' ctxt |> map Drule.zero_var_indexes