diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -3962,7 +3962,7 @@
         moreover
         from upd normal_s2
         have "{vn} \<subseteq> dom (locals (store (assign upd v s2)))"
-          by (auto simp add: assign_def Let_def lvar_def upd split: split_split)
+          by (auto simp add: assign_def Let_def lvar_def upd split: prod.split)
         ultimately
         show "nrm A \<subseteq> \<dots>"
           by (rule Un_least [elim_format]) (simp add: nrm_A)