diff -r 19b47bfac6ef -r 9e7d1c139569 src/HOL/HOLCF/Tr.thy
--- a/src/HOL/HOLCF/Tr.thy	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/HOLCF/Tr.thy	Thu Apr 18 17:07:01 2013 +0200
@@ -150,9 +150,10 @@
 apply (simp_all)
 done
 
+(* FIXME unused!? *)
 ML {*
-val split_If_tac =
-  simp_tac (HOL_basic_ss addsimps [@{thm If2_def} RS sym])
+fun split_If_tac ctxt =
+  simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm If2_def} RS sym])
     THEN' (split_tac [@{thm split_If2}])
 *}