diff -r c0844a30ea4e -r a7897aebbffc src/HOL/ex/Tarski.ML
--- a/src/HOL/ex/Tarski.ML	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/ex/Tarski.ML	Tue Jan 09 15:32:27 2001 +0100
@@ -400,7 +400,7 @@
 by (simp_tac (simpset() addsimps PO_simp) 1);
 qed "CLF_E2";
 
-Goal "f : CLF ``` {cl} ==> f : CLF ``` {dual cl}";
+Goal "f : CLF `` {cl} ==> f : CLF `` {dual cl}";
 by (afs [CLF_def, CL_dualCL, monotone_dual] 1); 
 by (afs [dualA_iff] 1);
 qed "CLF_dual";