src/Sequents/LK.thy

--- a/src/Sequents/LK.thy	Fri May 13 23:24:06 2011 +0200
+++ b/src/Sequents/LK.thy	Fri May 13 23:58:40 2011 +0200
@@ -216,6 +216,7 @@
   done
 
 use "simpdata.ML"
+setup {* Simplifier.map_simpset_global (K LK_ss) *}
 
 
 text {* To create substition rules *}