--- a/src/HOL/Modelcheck/CTL.thy Sat Aug 18 17:42:38 2007 +0200
+++ b/src/HOL/Modelcheck/CTL.thy Sat Aug 18 17:42:39 2007 +0200
@@ -17,6 +17,4 @@
EG ::"['a trans,'a pred]=> 'a pred"
"EG N f == nu (% Q. % u.(f u & CEX N Q u))"
-ML {* use_legacy_bindings (the_context ()) *}
-
end