--- a/src/FOL/IFOL.thy Thu Sep 29 00:58:54 2005 +0200 +++ b/src/FOL/IFOL.thy Thu Sep 29 00:58:55 2005 +0200 @@ -16,6 +16,7 @@ global classes "term" +final_consts term_class defaultsort "term" typedecl o