src/HOLCF/IOA/meta_theory/TLS.thy
changeset 26339 7825c83c9eff
parent 19741 f65265d71426
child 26359 6d437bde2f1d
--- a/src/HOLCF/IOA/meta_theory/TLS.thy	Wed Mar 19 22:28:17 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Wed Mar 19 22:47:35 2008 +0100
@@ -90,7 +90,7 @@
 lemmas [simp del] = ex_simps all_simps split_paired_Ex
 declare Let_def [simp]
 
-ML_setup {* change_claset (fn cs => cs delSWrapper "split_all_tac") *}
+declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
 
 
 subsection {* ex2seqC *}