src/HOL/ex/MT.thy
changeset 12338 de0f4a63baa5
parent 5102 8c782c25a11e
child 15450 43dfc914d1b8
--- a/src/HOL/ex/MT.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/ex/MT.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -31,19 +31,19 @@
   TyEnv
 
 arities 
-  Const :: term
+  Const :: type
 
-  ExVar :: term
-  Ex :: term
+  ExVar :: type
+  Ex :: type
 
-  TyConst :: term
-  Ty :: term
+  TyConst :: type
+  Ty :: type
 
-  Clos :: term
-  Val :: term
+  Clos :: type
+  Val :: type
 
-  ValEnv :: term
-  TyEnv :: term
+  ValEnv :: type
+  TyEnv :: type
 
 consts
   c_app :: [Const, Const] => Const