diff -r 235d65be79c9 -r ccafd7d193e7 src/HOL/Library/simps_case_conv.ML
--- a/src/HOL/Library/simps_case_conv.ML	Tue Jun 02 13:14:11 2015 +0200
+++ b/src/HOL/Library/simps_case_conv.ML	Tue Jun 02 13:14:36 2015 +0200
@@ -174,13 +174,14 @@
     THEN (forward_tac [refl_imp])
 
 fun do_split ctxt split =
-  let
-    val split' = split RS iffD1;
-    val split_rhs = Thm.concl_of (hd (snd (fst (Variable.import false [split'] ctxt))))
-  in if was_split split_rhs
-     then DETERM (apply_split ctxt split') THEN get_rules_once_split
-     else raise TERM ("malformed split rule", [split_rhs])
-  end
+  case try op RS (split, iffD1) of
+    NONE => raise TERM ("malformed split rule", [Thm.prop_of split])
+  | SOME split' =>
+      let val split_rhs = Thm.concl_of (hd (snd (fst (Variable.import false [split'] ctxt))))
+      in if was_split split_rhs
+         then DETERM (apply_split ctxt split') THEN get_rules_once_split
+         else raise TERM ("malformed split rule", [split_rhs])
+      end
 
 val atomize_meta_eq = forward_tac [meta_eq_to_obj_eq]