src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Thu Feb 28 13:19:25 2013 +0100
+++ b/src/HOL/HOL.thy	Thu Feb 28 13:24:51 2013 +0100
@@ -1987,8 +1987,6 @@
 subsection {* Legacy tactics and ML bindings *}
 
 ML {*
-fun strip_tac i = REPEAT (resolve_tac [impI, allI] i);
-
 (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
 local
   fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t