--- a/src/HOL/ex/atp_export.ML Mon Jun 27 14:56:26 2011 +0200
+++ b/src/HOL/ex/atp_export.ML Mon Jun 27 14:56:28 2011 +0200
@@ -158,8 +158,8 @@
facts0 |> map (fn ((_, loc), th) =>
((Thm.get_name_hint th, loc), prop_of th))
val (atp_problem, _, _, _, _, _, _) =
- prepare_atp_problem ctxt format Axiom Axiom type_sys true false true []
- @{prop False} facts
+ prepare_atp_problem ctxt format Axiom Axiom type_sys true true false true
+ [] @{prop False} facts
val atp_problem =
atp_problem
|> map (apsnd (filter_out (is_problem_line_tautology ctxt)))