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.
fixed bool vs. prop mismatch
authorblanchet
Wed, 31 Oct 2012 11:23:21 +0100
changeset 49994 ceceb403eb4e
parent 49993 80402e0e78e3
child 49995 3b7ad6153322
fixed bool vs. prop mismatch
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -889,14 +889,14 @@
                           if member (op = o apsnd fst) tainted s then
                             t |> s_not
                               |> fold exists_of (map Var (Term.add_vars t []))
-                              |> HOLogic.mk_Trueprop
                           else
-                            t |> HOLogic.mk_Trueprop
-                              |> close_form))
+                            t))
                   atp_proof
         fun prop_of_clause c =
           fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c)
                @{term False}
+          |> HOLogic.mk_Trueprop
+          |> close_form
         fun label_of_clause [name] = raw_label_for_name name
           | label_of_clause c = (space_implode "___" (map fst c), 0)
         fun maybe_show outer c =
isabelle