diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Bali/Example.thy	Tue Sep 07 10:05:19 2010 +0200
@@ -792,7 +792,7 @@
 lemma Base_fields_accessible[simp]:
  "accfield tprg S Base 
   = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Base))"
-apply (auto simp add: accfield_def expand_fun_eq Let_def 
+apply (auto simp add: accfield_def ext_iff Let_def 
                       accessible_in_RefT_simp
                       is_public_def
                       BaseCl_def
@@ -837,7 +837,7 @@
 lemma Ext_fields_accessible[simp]:
 "accfield tprg S Ext 
   = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Ext))"
-apply (auto simp add: accfield_def expand_fun_eq Let_def 
+apply (auto simp add: accfield_def ext_iff Let_def 
                       accessible_in_RefT_simp
                       is_public_def
                       BaseCl_def