src/HOL/Tools/Metis/metis_translate.ML
changeset 44088 3693baa6befb
parent 43983 c51b4196b5e6
child 44394 20bd9f90accc
--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Aug 09 09:05:21 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Aug 09 09:05:22 2011 +0200
@@ -197,7 +197,7 @@
     *)
     val (atp_problem, _, _, _, _, _, sym_tab) =
       prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
-                          (rpair []) false false [] @{prop False} props
+                          no_lambdasN false false [] @{prop False} props
     (*
     val _ = tracing ("ATP PROBLEM: " ^
                      cat_lines (tptp_lines_for_atp_problem CNF atp_problem))