Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_reconstruct.ML
changeset 43130 d73fc2e55308
parent 43127 a3f3b7a0e99e
child 43131 9e9420122f91 
--- 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
isabelle