--- a/src/HOL/W0/Type.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/W0/Type.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -10,7 +10,7 @@
 
 (* new class for structures containing type variables *)
 classes
-        type_struct < term 
+        type_struct < type
 
 (* type expressions *)
 datatype
@@ -23,7 +23,7 @@
 arities
         typ::type_struct
         list::(type_struct)type_struct
-        fun::(term,type_struct)type_struct
+        fun::(type,type_struct)type_struct
 
 (* substitutions *)