--- a/doc-src/IsarRef/Thy/Spec.thy Sat Oct 09 19:05:31 2010 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Sat Oct 09 19:49:19 2010 +0100
@@ -973,7 +973,7 @@
Usually the default sort is only changed when defining a new
object-logic. For example, the default sort in Isabelle/HOL is
- @{text type}, the class of all HOL types. %FIXME sort antiq?
+ @{class type}, the class of all HOL types.
When merging theories, the default sorts of the parents are
logically intersected, i.e.\ the representations as lists of classes