src/HOL/HOLCF/Tr.thy

--- a/src/HOL/HOLCF/Tr.thy	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/HOLCF/Tr.thy	Sun Nov 09 14:08:00 2014 +0100
@@ -154,7 +154,7 @@
 ML {*
 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}])
+    THEN' (split_tac ctxt [@{thm split_If2}])
 *}
 
 subsection "Rewriting of HOLCF operations to HOL functions"