--- 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