diff -r 6b38551d0798 -r f65265d71426 src/HOLCF/IOA/meta_theory/Pred.thy
--- a/src/HOLCF/IOA/meta_theory/Pred.thy	Sat May 27 21:18:51 2006 +0200
+++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Sun May 28 19:54:20 2006 +0200
@@ -67,6 +67,4 @@
 IMPLIES_def:
   "(P .--> Q) s == (P s) --> (Q s)"
 
-ML {* use_legacy_bindings (the_context ()) *}
-
 end