diff -r 43175817d83b -r a5db9779b026 src/HOL/Metis_Examples/Tarski.thy
--- a/src/HOL/Metis_Examples/Tarski.thy	Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy	Mon Feb 08 21:28:27 2010 +0100
@@ -78,11 +78,9 @@
           {S. S \<subseteq> pset cl &
            (| pset = S, order = induced S (order cl) |): CompleteLattice }"
 
-syntax
-  "@SL"  :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
-
-translations
-  "S <<= cl" == "S : sublattice `` {cl}"
+abbreviation
+  sublattice_syntax :: "['a set, 'a potype] => bool" ("_ <<= _" [51, 50] 50)
+  where "S <<= cl \<equiv> S : sublattice `` {cl}"
 
 constdefs
   dual :: "'a potype => 'a potype"