# HG changeset patch
# User wenzelm
# Date 1391274430 -3600
# Node ID 264d34c19bf29d2a47b5131c26e5f91665af6b0a
# Parent  cb5ef74b32f9a14fc85ba87e7bb34e4191f08831
unused;

diff -r cb5ef74b32f9 -r 264d34c19bf2 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 = {*