diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Sep 07 10:05:19 2010 +0200
@@ -98,7 +98,7 @@
 
 lemma set_set_swap:
   "r =!= r' \<Longrightarrow> set r x (set r' x' h) = set r' x' (set r x h)"
-  by (simp add: noteq_def set_def expand_fun_eq)
+  by (simp add: noteq_def set_def ext_iff)
 
 lemma alloc_set:
   "fst (alloc x (set r x' h)) = fst (alloc x h)"
@@ -126,7 +126,7 @@
 
 lemma present_set [simp]:
   "present (set r v h) = present h"
-  by (simp add: present_def expand_fun_eq)
+  by (simp add: present_def ext_iff)
 
 lemma noteq_I:
   "present h r \<Longrightarrow> \<not> present h r' \<Longrightarrow> r =!= r'"
@@ -220,7 +220,7 @@
 
 lemma array_get_set [simp]:
   "Array.get (set r v h) = Array.get h"
-  by (simp add: Array.get_def set_def expand_fun_eq)
+  by (simp add: Array.get_def set_def ext_iff)
 
 lemma get_update [simp]:
   "get (Array.update a i v h) r = get h r"
@@ -240,15 +240,15 @@
 
 lemma array_get_alloc [simp]: 
   "Array.get (snd (alloc v h)) = Array.get h"
-  by (simp add: Array.get_def alloc_def set_def Let_def expand_fun_eq)
+  by (simp add: Array.get_def alloc_def set_def Let_def ext_iff)
 
 lemma present_update [simp]: 
   "present (Array.update a i v h) = present h"
-  by (simp add: Array.update_def Array.set_def expand_fun_eq present_def)
+  by (simp add: Array.update_def Array.set_def ext_iff present_def)
 
 lemma array_present_set [simp]:
   "Array.present (set r v h) = Array.present h"
-  by (simp add: Array.present_def set_def expand_fun_eq)
+  by (simp add: Array.present_def set_def ext_iff)
 
 lemma array_present_alloc [simp]:
   "Array.present h a \<Longrightarrow> Array.present (snd (alloc v h)) a"