src/Sequents/LK0.thy

     |> fold_rev Cla.add_safe @{thms allR exL}
     |> fold_rev Cla.add_unsafe @{thms allL exR the_equality}
     |> Cla.get_pack;
 *}
 
-ML {*
-  fun lemma_tac th i =
-    rtac (@{thm thinR} RS @{thm cut}) i THEN
-    REPEAT (rtac @{thm thinL} i) THEN
-    rtac th i;
-*}
-
-
 method_setup fast_prop =
   {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.fast_tac (Cla.put_pack prop_pack ctxt))) *}
 
 method_setup fast_dup =
   {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.fast_tac (Cla.put_pack LK_dup_pack ctxt))) *}
 
 method_setup best_dup =
   {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack LK_dup_pack ctxt))) *}
+
+method_setup lem = {*
+  Attrib.thm >> (fn th => fn _ =>
+    SIMPLE_METHOD' (fn i =>
+      rtac (@{thm thinR} RS @{thm cut}) i THEN
+      REPEAT (rtac @{thm thinL} i) THEN
+      rtac th i))
+*}
 
 
 lemma mp_R:
   assumes major: "$H |- $E, $F, P --> Q"
     and minor: "$H |- $E, $F, P"