--- a/src/HOL/Bali/Example.thy Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Bali/Example.thy Mon Sep 13 11:13:15 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 ext_iff Let_def
+apply (auto simp add: accfield_def fun_eq_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 ext_iff Let_def
+apply (auto simp add: accfield_def fun_eq_iff Let_def
accessible_in_RefT_simp
is_public_def
BaseCl_def