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