diff -r 57dd0b45fc21 -r 7664e0916eec src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Mon Jul 27 17:44:55 2015 +0200
@@ -173,7 +173,7 @@
     let
       val cc = Thm.cterm_of ctxt c
       val ct = Thm.dest_arg (Thm.cprop_of th)
-    in resolve_tac ctxt [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
+    in resolve_tac ctxt [th] i (Thm.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
   | _ => resolve_tac ctxt [th] i st
 
 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,