src/Sequents/LK0.thy
changeset 27208 5fe899199f85
parent 27146 443c19953137
child 27239 f2f42f9fa09d
--- a/src/Sequents/LK0.thy	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/Sequents/LK0.thy	Sat Jun 14 23:19:51 2008 +0200
@@ -156,12 +156,12 @@
 
 ML {*
 (*Cut and thin, replacing the right-side formula*)
-fun cutR_tac s i =
-  res_inst_tac [ ("P", s) ] @{thm cut} i  THEN  rtac @{thm thinR} i
+fun cutR_tac ctxt s i =
+  RuleInsts.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 s i =
-  res_inst_tac [("P", s)] @{thm cut} i  THEN  rtac @{thm thinL} (i+1)
+fun cutL_tac ctxt s i =
+  RuleInsts.res_inst_tac ctxt [(("P", 0), s)] @{thm cut} i  THEN  rtac @{thm thinL} (i+1)
 *}