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/Tools/ATP/atp_proof_reconstruct.ML
changeset 59058 a78612c67ec0
parent 58653 4b44c227c0e0
child 59577 012c6165bbd2 
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -674,7 +674,7 @@
             val (haves, have_nots) =
               HOLogic.disjuncts t
               |> List.partition (exists_subterm (curry (op =) (Var v)))
-              |> pairself (fn lits => fold (curry s_disj) lits @{term False})
+              |> apply2 (fn lits => fold (curry s_disj) lits @{term False})
           in
             s_disj (HOLogic.all_const T
                 $ Abs (s, T, unskolem (safe_abstract_over (Var v, kill_skolem_arg haves))),
isabelle