diff -r 41aa67a045f7 -r 325300576da7 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Wed Nov 18 11:12:29 1998 +0100
+++ b/src/HOL/Set.ML	Wed Nov 18 15:10:46 1998 +0100
@@ -299,7 +299,7 @@
 val Pow_top = subset_refl RS PowI;             (* A : Pow(A) *)
 
 
-section "Set complement -- Compl";
+section "Set complement";
 
 qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : -A) = (c~:A)"
  (fn _ => [ (Blast_tac 1) ]);