--- 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