1.1 --- a/src/HOL/TLA/Intensional.thy	Sat Dec 01 18:51:46 2001 +0100
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Sat Dec 01 18:52:32 2001 +0100
     1.3 @@ -13,12 +13,12 @@
     1.4  Intensional  =  Main +
     1.5  
     1.6  axclass
     1.7 -  world < term
     1.8 +  world < type
     1.9  
    1.10  (** abstract syntax **)
    1.11  
    1.12  types
    1.13 -  ('w,'a) expr = 'w => 'a               (* intention: 'w::world, 'a::term *)
    1.14 +  ('w,'a) expr = 'w => 'a               (* intention: 'w::world, 'a::type *)
    1.15    'w form = ('w, bool) expr
    1.16  
    1.17  consts