--- a/src/FOL/IFOL.thy Fri Dec 30 16:56:56 2005 +0100 +++ b/src/FOL/IFOL.thy Fri Dec 30 16:56:57 2005 +0100 @@ -16,7 +16,7 @@ global classes "term" -final_consts term_class +finalconsts term_class defaultsort "term" typedecl o