--- a/src/CCL/CCL.thy Wed Jun 11 11:20:10 2008 +0200
+++ b/src/CCL/CCL.thy Wed Jun 11 15:40:20 2008 +0200
@@ -414,8 +414,7 @@
done
ML {*
- local val po_coinduct = thm "po_coinduct"
- in fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i end
+ fun po_coinduct_tac s i = res_inst_tac [("R",s)] @{thm po_coinduct} i
*}
@@ -460,13 +459,8 @@
done
ML {*
- local
- val eq_coinduct = thm "eq_coinduct"
- val eq_coinduct3 = thm "eq_coinduct3"
- in
- fun eq_coinduct_tac s i = res_inst_tac [("R",s)] eq_coinduct i
- fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] eq_coinduct3 i
- end
+ 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
*}