src/HOLCF/IOA/meta_theory/Traces.thy
changeset 26339 7825c83c9eff
parent 22808 a7daa74e2980
child 26359 6d437bde2f1d
--- a/src/HOLCF/IOA/meta_theory/Traces.thy	Wed Mar 19 22:28:17 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Wed Mar 19 22:47:35 2008 +0100
@@ -195,7 +195,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") *}
 
 lemmas exec_rws = executions_def is_exec_frag_def