src/Sequents/LK0.thy
changeset 27146 443c19953137
parent 22894 619b270607ac
child 27208 5fe899199f85
--- a/src/Sequents/LK0.thy	Wed Jun 11 11:20:10 2008 +0200
+++ b/src/Sequents/LK0.thy	Wed Jun 11 15:40:20 2008 +0200
@@ -155,21 +155,13 @@
   by (rule exchLS)
 
 ML {*
-local
-  val thinR = thm "thinR"
-  val thinL = thm "thinL"
-  val cut = thm "cut"
-in
-
 (*Cut and thin, replacing the right-side formula*)
 fun cutR_tac s i =
-  res_inst_tac [ ("P", s) ] cut i  THEN  rtac thinR i
+  res_inst_tac [ ("P", 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)] cut i  THEN  rtac thinL (i+1)
-
-end
+  res_inst_tac [("P", s)] @{thm cut} i  THEN  rtac @{thm thinL} (i+1)
 *}