changeset 59763 | 56d2c357e6b5 |
parent 59755 | f8d164ab0dc1 |
child 59780 | 23b67731f4f0 |
--- a/src/CCL/CCL.thy Fri Mar 20 11:53:22 2015 +0100 +++ b/src/CCL/CCL.thy Fri Mar 20 14:48:04 2015 +0100 @@ -475,7 +475,8 @@ method_setup eq_coinduct3 = {* Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => - SIMPLE_METHOD' (res_inst_tac ctxt [((("R", 0), Position.none), s)] @{thm eq_coinduct3})) + SIMPLE_METHOD' + (Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] @{thm eq_coinduct3})) *}