--- a/src/HOL/MiniML/Type.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/MiniML/Type.thy Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,7 @@
Type = Maybe +
(* new class for structures containing type variables *)
-axclass type_struct < term
+axclass type_struct < type
(* type expressions *)
@@ -33,7 +33,7 @@
instance typ::type_struct
instance type_scheme::type_struct
instance list::(type_struct)type_struct
-instance fun::(term,type_struct)type_struct
+instance fun::(type,type_struct)type_struct
(* free_tv s: the type variables occuring freely in the type structure s *)