src/Sequents/LK.thy
changeset 21428 f84cf8e9cad8
parent 17481 75166ebb619b
child 27149 123377499a8e
--- a/src/Sequents/LK.thy	Tue Nov 21 00:00:39 2006 +0100
+++ b/src/Sequents/LK.thy	Tue Nov 21 00:07:05 2006 +0100
@@ -25,8 +25,6 @@
   left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
                ==> (P, $H |- $F) == (P', $H' |- $F')"
 
-ML {* use_legacy_bindings (the_context ()) *}
-
 use "simpdata.ML"
 
 end