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.
close formula universally, to make SPASS happy
authorblanchet
Sun, 01 May 2011 18:37:25 +0200
changeset 42586 59e0ca92bb0b
parent 42585 723b9d1e8ba5
child 42587 4fbb1de05169
close formula universally, to make SPASS happy
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
@@ -795,7 +795,8 @@
              |> fold (curry (CombApp o swap)) bound_tms
              |> type_pred_combatom type_sys res_T
              |> mk_aquant AForall (bound_names ~~ bound_Ts)
-             |> formula_from_combformula ctxt type_sys,
+             |> formula_from_combformula ctxt type_sys
+             |> close_formula_universally,
              NONE, NONE)
   end
isabelle