--- a/src/Sequents/LK.thy Sat Jul 18 20:53:05 2015 +0200
+++ b/src/Sequents/LK.thy Sat Jul 18 20:54:56 2015 +0200
@@ -178,7 +178,7 @@
apply (lem p1)
apply safe
apply (tactic {*
- REPEAT (rtac @{thm cut} 1 THEN
+ REPEAT (resolve_tac @{context} @{thms cut} 1 THEN
DEPTH_SOLVE_1
(resolve_tac @{context} [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
Cla.safe_tac @{context} 1) *})
@@ -191,7 +191,7 @@
apply (lem p1)
apply safe
apply (tactic {*
- REPEAT (rtac @{thm cut} 1 THEN
+ REPEAT (resolve_tac @{context} @{thms cut} 1 THEN
DEPTH_SOLVE_1
(resolve_tac @{context} [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
Cla.safe_tac @{context} 1) *})