src/HOL/Tools/TFL/rules.ML

--- a/src/HOL/Tools/TFL/rules.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Tools/TFL/rules.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -389,7 +389,7 @@
 fun IT_EXISTS blist th =
    let val thy = Thm.theory_of_thm th
        val tych = cterm_of thy
-       val blist' = map (pairself Thm.term_of) blist
+       val blist' = map (apply2 Thm.term_of) blist
        fun ex v M  = cterm_of thy (USyntax.mk_exists{Bvar=v,Body = M})
 
   in