--- a/src/HOL/MicroJava/BV/Effect.thy Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy Tue Feb 23 16:25:08 2016 +0100
@@ -181,7 +181,7 @@
apply simp
apply simp
apply clarify
- apply (simp split: split_if_asm)
+ apply (simp split: if_split_asm)
apply (auto simp add: match_exception_entry_def)
done
@@ -189,7 +189,7 @@
"C \<in> set (match G X pc et) \<Longrightarrow> match_exception_table G C pc et \<noteq> None"
apply (induct et)
apply simp
- apply (simp split: split_if_asm)
+ apply (simp split: if_split_asm)
done
lemma xcpt_names_in_et: