changeset 59755 | f8d164ab0dc1 |
parent 59498 | 50b60f501b05 |
child 59763 | 56d2c357e6b5 |
--- a/src/HOL/Auth/Message.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/HOL/Auth/Message.thy Thu Mar 19 22:30:57 2015 +0100 @@ -866,7 +866,7 @@ (EVERY [ (*push in occurrences of X...*) (REPEAT o CHANGED) - (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1), + (res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1), (*...allowing further simplifications*) simp_tac ctxt 1, REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),