--- a/src/Sequents/LK0.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/Sequents/LK0.thy Mon Jun 16 22:13:39 2008 +0200
@@ -157,11 +157,11 @@
ML {*
(*Cut and thin, replacing the right-side formula*)
fun cutR_tac ctxt s i =
- RuleInsts.res_inst_tac ctxt [(("P", 0), s) ] @{thm cut} i THEN rtac @{thm thinR} i
+ res_inst_tac ctxt [(("P", 0), s) ] @{thm cut} i THEN rtac @{thm thinR} i
(*Cut and thin, replacing the left-side formula*)
fun cutL_tac ctxt s i =
- RuleInsts.res_inst_tac ctxt [(("P", 0), s)] @{thm cut} i THEN rtac @{thm thinL} (i+1)
+ res_inst_tac ctxt [(("P", 0), s)] @{thm cut} i THEN rtac @{thm thinL} (i+1)
*}