src/CCL/CCL.thy

   apply (rule EQgen_mono | assumption)+
   done
 
 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}))
 *}
 
 
 subsection {* Untyped Case Analysis and Other Facts *}