diff -r 97ff9276e12d -r 66df76dd2640 src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Mon Feb 24 23:17:55 2014 +0000
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Tue Feb 25 15:02:19 2014 +0100
@@ -447,16 +447,6 @@
    end
   
   fun rewrs_imp rules = first_imp (map rewr_imp rules)
-
-  fun map_interrupt f l =
-    let
-      fun map_interrupt' _ [] l = SOME (rev l)
-       | map_interrupt' f (x::xs) l = (case f x of
-        NONE => NONE
-        | SOME v => map_interrupt' f xs (v::l))
-    in
-      map_interrupt' f l []
-    end
 in
 
   (*