src/Provers/hypsubst.ML

         val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi);
         val rl' = Thm.lift_rule cBi rl;
         val (ixn, T) = dest_Var (Term.head_of (Data.dest_Trueprop
           (Logic.strip_assums_concl (Thm.prop_of rl'))));
         val (v1, v2) = Data.dest_eq (Data.dest_Trueprop
-          (Logic.strip_assums_concl (hd (Thm.prems_of rl'))));
+          (Logic.strip_assums_concl (hd (Thm.take_prems_of 1 rl'))));
         val (Ts, V) = split_last (Term.binder_types T);
         val u =
           fold_rev Term.abs (ps @ [("x", U)])
             (case (if b then t else t') of
               Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)