--- a/src/CCL/CCL.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/CCL/CCL.thy Mon Jun 16 22:13:39 2008 +0200
@@ -415,7 +415,7 @@
ML {*
fun po_coinduct_tac ctxt s i =
- RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm po_coinduct} i
+ res_inst_tac ctxt [(("R", 0), s)] @{thm po_coinduct} i
*}
@@ -460,11 +460,8 @@
done
ML {*
- 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
+ fun eq_coinduct_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct} i
+ fun eq_coinduct3_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3} i
*}