changeset 58963 | 26bf09b95dda |
parent 56245 | 84fc7dfa3cd4 |
child 59170 | de18f8b1a5a2 |
--- a/src/FOLP/simp.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/FOLP/simp.ML Mon Nov 10 21:49:48 2014 +0100 @@ -451,7 +451,7 @@ thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs) end | NONE => if more - then rew((lhs_net_tac anet i THEN assume_tac i) thm, + then rew((lhs_net_tac anet i THEN atac i) thm, thm,ss,anet,ats,cs,false) else (ss,thm,anet,ats,cs);