# HG changeset patch
# User noschinl
# Date 1433316769 -7200
# Node ID 2e1c1968b38e15be06f008aa6107e24ee6b41dc8
# Parent  ccafd7d193e7d7b65797c6d62d9bd4be37549b56# Parent  838025c6e278d2daed6d1fe4a301a06125f1383b
merged

diff -r 838025c6e278 -r 2e1c1968b38e src/HOL/Library/simps_case_conv.ML
--- a/src/HOL/Library/simps_case_conv.ML	Mon Jun 01 18:59:22 2015 +0200
+++ b/src/HOL/Library/simps_case_conv.ML	Wed Jun 03 09:32:49 2015 +0200
@@ -174,21 +174,24 @@
     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]
 
 in
 
 fun gen_to_simps ctxt splitthms thm =
-  Seq.list_of ((TRY atomize_meta_eq
-                 THEN (REPEAT (FIRST (map (do_split ctxt) splitthms)))) thm)
+  let val splitthms' = filter (fn t => not (Thm.eq_thm (t, Drule.dummy_thm))) splitthms
+  in
+    Seq.list_of ((TRY atomize_meta_eq THEN (REPEAT (FIRST (map (do_split ctxt) splitthms')))) thm)
+  end
 
 fun to_simps ctxt thm =
   let