changeset 52131 | 366fa32ee2a3 |
parent 51798 | ad3a241def73 |
child 56245 | 84fc7dfa3cd4 |
--- a/src/Provers/hypsubst.ML Fri May 24 16:42:57 2013 +0200 +++ b/src/Provers/hypsubst.ML Fri May 24 17:00:46 2013 +0200 @@ -224,7 +224,7 @@ |> Logic.strip_assums_concl |> Data.dest_Trueprop |> Data.dest_imp; val (r', tac) = - if Pattern.aeconv (hyp, hyp') + if Envir.aeconv (hyp, hyp') then (r, imp_intr_tac i THEN rotate_tac ~1 i) else (*leave affected hyps at end*) (r + 1, imp_intr_tac i); in