--- a/src/HOLCF/IOA/ABP/Impl_finite.thy Sat May 27 19:49:07 2006 +0200
+++ b/src/HOLCF/IOA/ABP/Impl_finite.thy Sat May 27 19:49:36 2006 +0200
@@ -32,6 +32,4 @@
rsch_fin :: "'m impl_fin_state => bool list"
"rsch_fin == snd o snd o snd"
-ML {* use_legacy_bindings (the_context ()) *}
-
end