Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
compile
authorblanchet
Thu, 09 Jun 2011 00:16:28 +0200
changeset 43305 8b59c1d87fd6
parent 43304 6901ebafbb8d
child 43306 03e6da81aee6
compile
src/HOL/ex/atp_export.ML file | annotate | diff | comparison | revisions 
--- 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