diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Sun Jul 05 15:02:30 2015 +0200
@@ -44,10 +44,10 @@
    "Sledgehammer_Util".) *)
 fun transform_elim_theorem th =
   (case Thm.concl_of th of    (*conclusion variable*)
-    @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
-      Thm.instantiate ([], [(Thm.cterm_of @{theory_context HOL} v, cfalse)]) th
-  | v as Var(_, @{typ prop}) =>
-      Thm.instantiate ([], [(Thm.cterm_of @{theory_context HOL} v, ctp_false)]) th
+    @{const Trueprop} $ (Var (v as (_, @{typ bool}))) =>
+      Thm.instantiate ([], [(v, cfalse)]) th
+  | Var (v as (_, @{typ prop})) =>
+      Thm.instantiate ([], [(v, ctp_false)]) th
   | _ => th)
 
 
@@ -375,9 +375,7 @@
        th ctxt
     val (cnf_ths, ctxt) = clausify nnf_th
     fun intr_imp ct th =
-      Thm.instantiate ([], map (apply2 (Thm.cterm_of ctxt))
-                               [(Var (("i", 0), @{typ nat}),
-                                 HOLogic.mk_nat ax_no)])
+      Thm.instantiate ([], [((("i", 0), @{typ nat}), Thm.cterm_of ctxt (HOLogic.mk_nat ax_no))])
                       (zero_var_indexes @{thm skolem_COMBK_D})
       RS Thm.implies_intr ct th
   in