src/HOL/Library/simps_case_conv.ML

--- a/src/HOL/Library/simps_case_conv.ML	Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Library/simps_case_conv.ML	Sun Nov 09 14:08:00 2014 +0100
@@ -88,7 +88,7 @@
 
 fun tac ctxt {splits, intros, defs} =
   let val ctxt' = Classical.addSIs (ctxt, intros) in
-    REPEAT_DETERM1 (FIRSTGOAL (split_tac splits))
+    REPEAT_DETERM1 (FIRSTGOAL (split_tac ctxt splits))
     THEN Local_Defs.unfold_tac ctxt defs
     THEN safe_tac ctxt'
   end