--- a/src/Sequents/LK0.thy Mon Mar 23 10:16:20 2015 +0100
+++ b/src/Sequents/LK0.thy Mon Mar 23 13:30:59 2015 +0100
@@ -153,12 +153,12 @@
ML {*
(*Cut and thin, replacing the right-side formula*)
fun cutR_tac ctxt s i =
- Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s) ] @{thm cut} i THEN
+ Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] [] @{thm cut} i THEN
rtac @{thm thinR} i
(*Cut and thin, replacing the left-side formula*)
fun cutL_tac ctxt s i =
- Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] @{thm cut} i THEN
+ Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] [] @{thm cut} i THEN
rtac @{thm thinL} (i + 1)
*}