# HG changeset patch
# User noschinl
# Date 1433243651 -7200
# Node ID 235d65be79c938720144d277a5d65aa3cb204f36
# Parent  f0b2457bf68e386cfa7950c0f5bc354d4391bc65
simps_of_case: allow Drule.dummy_thm as ignored split rule

diff -r f0b2457bf68e -r 235d65be79c9 src/HOL/Library/simps_case_conv.ML
--- a/src/HOL/Library/simps_case_conv.ML	Mon Jun 01 18:07:36 2015 +0200
+++ b/src/HOL/Library/simps_case_conv.ML	Tue Jun 02 13:14:11 2015 +0200
@@ -187,8 +187,10 @@
 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