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_problem_generate.ML
changeset 74760 ef9f95d055f6
parent 74759 32e95d996acc
child 74890 11e34ffc65e4 
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Nov 11 12:02:08 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Nov 11 15:34:02 2021 +0100
@@ -1270,7 +1270,7 @@
         let val argc = length args in
           if has_ite andalso s = "c_If" andalso argc >= 3 then
             IConst (`I tptp_ite, T, [])
-          else if is_fool andalso s = "c_Let" andalso argc = 2 then
+          else if is_fool andalso s = "c_Let" andalso argc >= 2 then
             IConst (`I tptp_let, T, [])
           else
             (case proxify_const s of
isabelle