changeset 27147 | 62ab1968c1f4 |
parent 27105 | 5f139027c365 |
child 27154 | 026f3db3f5c6 |
--- a/src/HOL/Auth/Message.thy Wed Jun 11 15:40:20 2008 +0200 +++ b/src/HOL/Auth/Message.thy Wed Jun 11 15:40:44 2008 +0200 @@ -882,7 +882,8 @@ (EVERY [ (*push in occurrences of X...*) (REPEAT o CHANGED) - (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1), + (RuleInsts.res_inst_tac (Simplifier.the_context ss) + [(("x", 1), "X")] (insert_commute RS ssubst) 1), (*...allowing further simplifications*) simp_tac ss 1, REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),