src/Sequents/LK0.thy
changeset 27239 f2f42f9fa09d
parent 27208 5fe899199f85
child 30510 4120fc59dd85
--- 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)
 *}