--- a/src/HOL/MicroJava/DFA/Typing_Framework_err.thy Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/MicroJava/DFA/Typing_Framework_err.thy Tue Feb 23 16:25:08 2016 +0100
@@ -70,7 +70,7 @@
apply clarify
apply (erule allE, erule impE, assumption)
apply (case_tac s)
- apply (auto simp add: map_snd_def split: split_if_asm)
+ apply (auto simp add: map_snd_def split: if_split_asm)
done
@@ -150,7 +150,7 @@
apply simp
apply (drule in_errorD)
apply simp
-apply (simp add: map_snd_def split: split_if_asm)
+apply (simp add: map_snd_def split: if_split_asm)
apply fast
apply (drule in_errorD)
apply simp