Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/atp_export.ML
changeset 43305 8b59c1d87fd6
parent 43276 91bf67e0e755
child 43351 b19d95b4d736 
--- 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) =>
isabelle