changeset 59755 | f8d164ab0dc1 |
parent 59499 | 14095f771781 |
child 59763 | 56d2c357e6b5 |
--- a/src/CCL/CCL.thy Thu Mar 19 17:25:57 2015 +0100 +++ b/src/CCL/CCL.thy Thu Mar 19 22:30:57 2015 +0100 @@ -475,7 +475,7 @@ method_setup eq_coinduct3 = {* Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => - SIMPLE_METHOD' (res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3})) + SIMPLE_METHOD' (res_inst_tac ctxt [((("R", 0), Position.none), s)] @{thm eq_coinduct3})) *}