diff -r b286e8f47560 -r 28e37eab4e6f src/HOL/ex/Tarski.thy
--- a/src/HOL/ex/Tarski.thy	Wed Oct 10 15:27:10 2012 +0200
+++ b/src/HOL/ex/Tarski.thy	Wed Oct 10 15:39:01 2012 +0200
@@ -119,7 +119,7 @@
 locale CL = S +
   assumes cl_co:  "cl : CompleteLattice"
 
-sublocale CL < PO
+sublocale CL < po: PO
 apply (simp_all add: A_def r_def)
 apply unfold_locales
 using cl_co unfolding CompleteLattice_def by auto
@@ -130,7 +130,7 @@
   assumes f_cl:  "(cl,f) : CLF_set" (*was the equivalent "f : CLF_set``{cl}"*)
   defines P_def: "P == fix f A"
 
-sublocale CLF < CL
+sublocale CLF < cl: CL
 apply (simp_all add: A_def r_def)
 apply unfold_locales
 using f_cl unfolding CLF_set_def by auto