src/HOL/MicroJava/JVM/JVMExceptions.thy

--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -52,7 +52,7 @@
 \<close>
 lemma match_exception_table_in_et:
   "match_exception_table G C pc et = Some pc' \<Longrightarrow> \<exists>e \<in> set et. pc' = fst (snd (snd e))"
-  by (induct et) (auto split: split_if_asm)
+  by (induct et) (auto split: if_split_asm)
 
 
 end