src/HOL/TLA/Intensional.thy

--- a/src/HOL/TLA/Intensional.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/TLA/Intensional.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -13,12 +13,12 @@
 Intensional  =  Main +
 
 axclass
-  world < term
+  world < type
 
 (** abstract syntax **)
 
 types
-  ('w,'a) expr = 'w => 'a               (* intention: 'w::world, 'a::term *)
+  ('w,'a) expr = 'w => 'a               (* intention: 'w::world, 'a::type *)
   'w form = ('w, bool) expr
 
 consts