src/HOL/Tools/Lifting/lifting_term.ML

         Thm.instantiate (Thm.match (lhs_rule, lhs_ct)) rule2
           handle Pattern.MATCH => raise CTERM ("rewr_imp", [lhs_rule, lhs_ct])
    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
 
   (*
     ctm - of the form "[POS|NEG] (par_R OO T) t f) ?X", where par_R is a parametricity transfer 
     relation for t and T is a transfer relation between t and f, which consists only from