diff -r 8758895ea413 -r aa5dfb03eb1e src/HOLCF/Sum_Cpo.thy
--- a/src/HOLCF/Sum_Cpo.thy	Mon Mar 22 19:29:11 2010 +0100
+++ b/src/HOLCF/Sum_Cpo.thy	Mon Mar 22 12:52:51 2010 -0700
@@ -8,7 +8,7 @@
 imports Bifinite
 begin
 
-subsection {* Ordering on type @{typ "'a + 'b"} *}
+subsection {* Ordering on sum type *}
 
 instantiation "+" :: (below, below) below
 begin
@@ -128,7 +128,7 @@
  apply (erule cpo_lubI)
 done
 
-subsection {* Continuity of @{term Inl}, @{term Inr}, @{term sum_case} *}
+subsection {* Continuity of \emph{Inl}, \emph{Inr}, and case function *}
 
 lemma cont_Inl: "cont Inl"
 by (intro contI is_lub_Inl cpo_lubI)