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/Meson/meson_clausify.ML
changeset 59058 a78612c67ec0
parent 58839 ccda99401bc8
child 59165 115965966e15 
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -375,7 +375,7 @@
                th ctxt ctxt
     val (cnf_ths, ctxt) = clausify nnf_th
     fun intr_imp ct th =
-      Thm.instantiate ([], map (pairself (cterm_of thy))
+      Thm.instantiate ([], map (apply2 (cterm_of thy))
                                [(Var (("i", 0), @{typ nat}),
                                  HOLogic.mk_nat ax_no)])
                       (zero_var_indexes @{thm skolem_COMBK_D})
isabelle