src/Provers/hypsubst.ML
changeset 42366 2305c70ec9b1
parent 42364 8c674b3b8e44
child 42799 4e33894aec6d
equal deleted inserted replaced
42365:bfd28ba57859 42366:2305c70ec9b1
   217   let
   217   let
   218     fun imptac (r, []) st = reverse_n_tac r i st
   218     fun imptac (r, []) st = reverse_n_tac r i st
   219       | imptac (r, hyp::hyps) st =
   219       | imptac (r, hyp::hyps) st =
   220           let
   220           let
   221             val (hyp', _) =
   221             val (hyp', _) =
   222               nth (prems_of st) (i - 1)
   222               term_of (Thm.cprem_of st i)
   223               |> Logic.strip_assums_concl
   223               |> Logic.strip_assums_concl
   224               |> Data.dest_Trueprop |> Data.dest_imp;
   224               |> Data.dest_Trueprop |> Data.dest_imp;
   225             val (r', tac) =
   225             val (r', tac) =
   226               if Pattern.aeconv (hyp, hyp')
   226               if Pattern.aeconv (hyp, hyp')
   227               then (r, imp_intr_tac i THEN rotate_tac ~1 i)
   227               then (r, imp_intr_tac i THEN rotate_tac ~1 i)