diff -r 4301f1c123d6 -r d73fc2e55308 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -450,7 +450,7 @@
             else if s' = predicator_name then
               do_term [] (SOME @{typ bool}) (hd us)
             else if s' = app_op_name then
-              do_term (nth us 1 :: extra_us) opt_T (hd us)
+              do_term (List.last us :: extra_us) opt_T (nth us (length us - 2))
             else if s' = type_pred_name then
               @{const True} (* ignore type predicates *)
             else