--- a/src/HOL/Tools/Metis/metis_generate.ML Sat Dec 19 20:02:51 2015 +0100
+++ b/src/HOL/Tools/Metis/metis_generate.ML Sat Dec 19 20:02:51 2015 +0100
@@ -227,7 +227,7 @@
*)
val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
val (atp_problem, _, lifted, sym_tab) =
- generate_atp_problem ctxt CNF Hypothesis type_enc Metis lam_trans false false false []
+ generate_atp_problem ctxt true CNF Hypothesis type_enc Metis lam_trans false false false []
@{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^