# HG changeset patch
# User noschinl
# Date 1433243676 -7200
# Node ID ccafd7d193e7d7b65797c6d62d9bd4be37549b56
# Parent  235d65be79c938720144d277a5d65aa3cb204f36
simps_of_case: Better error if split rule is not an equality

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]