src/CCL/CCL.thy
changeset 27146 443c19953137
parent 26342 0f65fa163304
child 27208 5fe899199f85
--- 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
 *}