--- a/src/HOL/Tools/Metis/metis_translate.ML Sun Jul 17 14:11:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Sun Jul 17 14:11:35 2011 +0200
@@ -197,8 +197,8 @@
*)
val (atp_problem, _, _, _, _, _, sym_tab) =
prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
- (map (introduce_combinators ctxt)) false false []
- @{prop False} props
+ (map (introduce_combinators ctxt o snd)) false false
+ [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
cat_lines (tptp_lines_for_atp_problem CNF atp_problem))