src/HOLCF/IOA/meta_theory/CompoTraces.thy
changeset 26339 7825c83c9eff
parent 19741 f65265d71426
child 26359 6d437bde2f1d
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed Mar 19 22:28:17 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed Mar 19 22:47:35 2008 +0100
@@ -68,7 +68,7 @@
   "Finite (mksch A B$tr$x$y) --> Finite tr"
 
 
-ML_setup {* change_simpset (fn ss => ss setmksym (K NONE)) *}
+declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K NONE)) *}
 
 
 subsection "mksch rewrite rules"
@@ -967,7 +967,7 @@
 done
 
 
-ML_setup {* change_simpset (fn ss => ss setmksym (SOME o symmetric_fun)) *}
+declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (SOME o symmetric_fun)) *}
 
 
 end