diff -r 6b94c39b7366 -r e9e7209eb375 src/HOL/ex/Tarski.thy
--- a/src/HOL/ex/Tarski.thy	Thu Mar 01 17:13:54 2012 +0000
+++ b/src/HOL/ex/Tarski.thy	Thu Mar 01 19:34:52 2012 +0100
@@ -227,10 +227,10 @@
 by (simp add: glb_def greatest_def isGlb_def some_eq_ex [symmetric])
 
 lemma isGlb_dual_isLub: "isGlb S cl = isLub S (dual cl)"
-by (simp add: isLub_def isGlb_def dual_def converse_def)
+by (simp add: isLub_def isGlb_def dual_def converse_unfold)
 
 lemma isLub_dual_isGlb: "isLub S cl = isGlb S (dual cl)"
-by (simp add: isLub_def isGlb_def dual_def converse_def)
+by (simp add: isLub_def isGlb_def dual_def converse_unfold)
 
 lemma (in PO) dualPO: "dual cl \<in> PartialOrder"
 apply (insert cl_po)
@@ -251,10 +251,10 @@
 done
 
 lemma lub_dual_glb: "lub S cl = glb S (dual cl)"
-by (simp add: lub_def glb_def least_def greatest_def dual_def converse_def)
+by (simp add: lub_def glb_def least_def greatest_def dual_def converse_unfold)
 
 lemma glb_dual_lub: "glb S cl = lub S (dual cl)"
-by (simp add: lub_def glb_def least_def greatest_def dual_def converse_def)
+by (simp add: lub_def glb_def least_def greatest_def dual_def converse_unfold)
 
 lemma CL_subset_PO: "CompleteLattice \<subseteq> PartialOrder"
 by (simp add: PartialOrder_def CompleteLattice_def, fast)