--- a/src/CCL/CCL.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/CCL/CCL.thy Sat Jun 14 23:19:51 2008 +0200
@@ -414,7 +414,8 @@
done
ML {*
- fun po_coinduct_tac s i = res_inst_tac [("R",s)] @{thm po_coinduct} i
+ fun po_coinduct_tac ctxt s i =
+ RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm po_coinduct} i
*}
@@ -459,8 +460,11 @@
done
ML {*
- fun eq_coinduct_tac s i = res_inst_tac [("R",s)] @{thm eq_coinduct} i
- fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] @{thm eq_coinduct3} i
+ fun eq_coinduct_tac ctxt s i =
+ RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct} i
+
+ fun eq_coinduct3_tac ctxt s i =
+ RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3} i
*}