src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Tue Dec 22 15:38:59 2015 +0100
+++ b/src/HOL/HOL.thy	Tue Dec 22 15:39:01 2015 +0100
@@ -1974,8 +1974,8 @@
       | wrong_prem (Bound _) = true
       | wrong_prem _ = false;
     val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
+    fun smp i = funpow i (fn m => filter_right ([spec] RL m)) [mp];
   in
-    fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
     fun smp_tac ctxt j = EVERY' [dresolve_tac ctxt (smp j), assume_tac ctxt];
   end;