src/CCL/CCL.thy

--- a/src/CCL/CCL.thy	Mon Mar 23 10:16:20 2015 +0100
+++ b/src/CCL/CCL.thy	Mon Mar 23 13:30:59 2015 +0100
@@ -476,7 +476,7 @@
 method_setup eq_coinduct3 = {*
   Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt =>
     SIMPLE_METHOD'
-      (Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] @{thm eq_coinduct3}))
+      (Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] [] @{thm eq_coinduct3}))
 *}