# HG changeset patch
# User blanchet
# Date 1307571388 -7200
# Node ID 8b59c1d87fd684bbe3174eff23bcb5803b6bbd89
# Parent  6901ebafbb8d0b4f43cc363bb37318f44d064ae4
compile

diff -r 6901ebafbb8d -r 8b59c1d87fd6 src/HOL/ex/atp_export.ML
--- a/src/HOL/ex/atp_export.ML	Thu Jun 09 00:16:28 2011 +0200
+++ b/src/HOL/ex/atp_export.ML	Thu Jun 09 00:16:28 2011 +0200
@@ -104,7 +104,7 @@
                         ((Thm.get_name_hint th, loc), prop_of th))
     val (atp_problem, _, _, _, _, _, _) =
       ATP_Translate.prepare_atp_problem ctxt format
-          ATP_Problem.Axiom ATP_Problem.Axiom type_sys false true []
+          ATP_Problem.Axiom ATP_Problem.Axiom type_sys false false true []
           @{prop False} facts
     val infers =
       facts0 |> map (fn (_, th) =>