diff -r c0844a30ea4e -r a7897aebbffc src/HOL/ex/Tarski.thy
--- a/src/HOL/ex/Tarski.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/ex/Tarski.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -94,7 +94,7 @@
   "@SL"  :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
 
 translations
-  "S <<= cl" == "S : sublattice ``` {cl}"
+  "S <<= cl" == "S : sublattice `` {cl}"
 
 constdefs
   dual :: "'a potype => 'a potype"
@@ -121,7 +121,7 @@
   f :: "'a => 'a"
   P :: "'a set"
 assumes 
-  f_cl "f : CLF```{cl}"
+  f_cl "f : CLF``{cl}"
 defines
   P_def "P == fix f A"