--- a/src/HOLCF/IOA/NTP/Correctness.thy Wed Mar 19 22:28:17 2008 +0100
+++ b/src/HOLCF/IOA/NTP/Correctness.thy Wed Mar 19 22:47:35 2008 +0100
@@ -14,9 +14,9 @@
"hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
else tl(sq(sen s)))"
-ML_setup {*
-(* repeated from Traces.ML *)
-change_claset (fn cs => cs delSWrapper "split_all_tac")
+declaration {* fn _ =>
+ (* repeated from Traces.ML *)
+ Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")
*}
lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas