--- a/src/HOL/Tools/Metis/metis_generate.ML Sun May 13 16:31:01 2012 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML Sun May 13 16:31:01 2012 +0200
@@ -242,8 +242,8 @@
*)
val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
val (atp_problem, _, _, lifted, sym_tab) =
- prepare_atp_problem ctxt CNF Hypothesis Hypothesis type_enc false
- lam_trans false false false [] @{prop False} props
+ prepare_atp_problem ctxt CNF Hypothesis type_enc false lam_trans false
+ false false [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
cat_lines (lines_for_atp_problem CNF atp_problem))