src/HOL/Library/FinFun.thy

--- a/src/HOL/Library/FinFun.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Library/FinFun.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -578,7 +578,7 @@
   have gg: "g = ?g" unfolding g
   proof(rule the_equality)
     from f y bfin show "?the f ?g"
-      by(auto)(simp add: restrict_map_def ran_def split: split_if_asm)
+      by(auto)(simp add: restrict_map_def ran_def split: if_split_asm)
   next
     fix g'
     assume "?the f g'"
@@ -1308,7 +1308,7 @@
   case (update f a b)
   have "{x. finfun_dom f(a $:= b) $ x} =
     (if b = finfun_default f then {x. finfun_dom f $ x} - {a} else insert a {x. finfun_dom f $ x})"
-    by (auto simp add: finfun_upd_apply split: split_if_asm)
+    by (auto simp add: finfun_upd_apply split: if_split_asm)
   thus ?case using update by simp
 qed
 
@@ -1372,7 +1372,7 @@
         have "set (insort_insert a xs) = insert a (set xs)" by(simp add: set_insort_insert)
         also note eq also
         have "insert a {x. finfun_dom f(a $:= b) $ x} = {x. finfun_dom f $ x}" using True
-          by(auto simp add: finfun_upd_apply split: split_if_asm)
+          by(auto simp add: finfun_upd_apply split: if_split_asm)
         finally show 1: "set (insort_insert a xs) = {x. finfun_dom f $ x} \<and> sorted (insort_insert a xs) \<and> distinct (insort_insert a xs)"
           by(simp add: sorted_insort_insert distinct_insort_insert)
 
@@ -1415,7 +1415,7 @@
         have "set (remove1 a xs) = set xs - {a}" by simp
         also note eq also
         have "{x. finfun_dom f(a $:= b) $ x} - {a} = {x. finfun_dom f $ x}" using False
-          by(auto simp add: finfun_upd_apply split: split_if_asm)
+          by(auto simp add: finfun_upd_apply split: if_split_asm)
         finally show 1: "set (remove1 a xs) = {x. finfun_dom f $ x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)"
           by(simp add: sorted_remove1)
         
@@ -1427,7 +1427,7 @@
         by (simp add: insort_insert_insort insort_remove1)
     qed
   qed
-qed (auto simp add: distinct_finfun_to_list sorted_finfun_to_list sorted_remove1 set_insort_insert sorted_insort_insert distinct_insort_insert finfun_upd_apply split: split_if_asm)
+qed (auto simp add: distinct_finfun_to_list sorted_finfun_to_list sorted_remove1 set_insort_insert sorted_insort_insert distinct_insort_insert finfun_upd_apply split: if_split_asm)
 
 lemma finfun_to_list_update_code [code]:
   "finfun_to_list (finfun_update_code f a b) = 
@@ -1489,7 +1489,7 @@
     hence "finite (range ?f)" 
       by(rule finite_subset[rotated 1])(auto simp add: F_def finfun_def \<open>b1 \<noteq> b2\<close> intro!: exI[where x=b2])
     thus "finite (UNIV :: 'a set)"
-      by(rule finite_imageD)(auto intro: inj_onI simp add: fun_eq_iff \<open>b1 \<noteq> b2\<close> split: split_if_asm)
+      by(rule finite_imageD)(auto intro: inj_onI simp add: fun_eq_iff \<open>b1 \<noteq> b2\<close> split: if_split_asm)
     
     from finite have "finite (range (\<lambda>b. ((K$ b) :: 'a \<Rightarrow>f 'b)))"
       by(rule finite_subset[rotated 1]) simp