src/Sequents/ILL.thy

--- a/src/Sequents/ILL.thy	Sat Feb 01 18:05:03 2014 +0100
+++ b/src/Sequents/ILL.thy	Sat Feb 01 18:07:10 2014 +0100
@@ -135,9 +135,6 @@
       derelict weaken promote1 promote2
       context1 context4a context4b}
     |> Cla.get_pack;
-  
-  fun promote_tac i =
-    REPEAT (resolve_tac @{thms promote0 promote1 promote2} i);
 *}
 
 method_setup best_lazy = {*