src/CCL/CCL.thy
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}))
 *}