--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jul 30 14:03:13 2014 +0200
@@ -239,13 +239,13 @@
in
if textual then
(case ts of
- [fst, lst] =>
- if loose_aconv (fst, lst) then
+ [t1, t2] =>
+ if loose_aconv (t1, t2) then
@{const True}
- else if Term.aconv_untyped (lst, @{const True}) then
- fst
- else if Term.aconv_untyped (fst, @{const True}) then
- lst
+ else if Term.aconv_untyped (t2, @{const True}) then
+ t1
+ else if Term.aconv_untyped (t1, @{const True}) then
+ t2
else
equal_term ts
| _ => equal_term ts)