--- a/src/HOLCF/Tr.thy Tue May 31 11:53:11 2005 +0200
+++ b/src/HOLCF/Tr.thy Tue May 31 11:53:12 2005 +0200
@@ -132,7 +132,7 @@
apply (simp_all)
done
-ML_setup {*
+ML {*
val split_If_tac =
simp_tac (HOL_basic_ss addsimps [symmetric (thm "If2_def")])
THEN' (split_tac [thm "split_If2"])