src/Pure/logic.ML

       | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   in lift [] end;
 
 (*Strips assumptions in goal, yielding list of hypotheses.   *)
-fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B
-  | strip_assums_hyp (Const("all",_)$Abs(a,T,t)) = strip_assums_hyp t
-  | strip_assums_hyp B = [];
+fun strip_assums_hyp B =
+  let
+    fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B
+      | strip Hs (Const ("all", _) $ Abs (a, T, t)) =
+          strip (map (incr_boundvars 1) Hs) t
+      | strip Hs B = rev Hs
+  in strip [] B end;
 
 (*Strips assumptions in goal, yielding conclusion.   *)
 fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
   | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
   | strip_assums_concl B = B;