src/HOL/Tools/Qelim/qelim.ML

--- a/src/HOL/Tools/Qelim/qelim.ML	Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Mon Jul 27 17:44:55 2015 +0200
@@ -45,7 +45,7 @@
     let
      val p = Thm.dest_arg p
      val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
-     val th = instantiate' [SOME T] [SOME p] all_not_ex
+     val th = Thm.instantiate' [SOME T] [SOME p] all_not_ex
     in Thm.transitive th (conv env (Thm.rhs_of th))
     end
   | _ => atcv env p