--- a/doc-src/IsarRef/Thy/document/Spec.tex Sat Oct 09 19:05:31 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Sat Oct 09 19:49:19 2010 +0100
@@ -1010,7 +1010,7 @@
Usually the default sort is only changed when defining a new
object-logic. For example, the default sort in Isabelle/HOL is
- \isa{type}, the class of all HOL types. %FIXME sort antiq?
+ \isa{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