Strange error in loading a theory

[Ajay Chander <ajayc@stanford.edu>]

Folks,

I just installed PVS on my Debian box, and am trying to run the proofs of 
theories created with 2.3 with the new version.  At the bottom is a sample 
file that gives this parse error at the first line:  "!ID! when expecting 
THEORY or DATATYPE", which is quite puzzling.  Any help?

Thanks,


world_state: THEORY
 BEGIN

  object: TYPE+

  right: TYPE+

  preWS: TYPE =
     [# ob: set[object],
         r: set[right],
         A: [ [object, right] -> set[[object, nat]] ],  % powerset
         D: [ [object, right, object] -> set[[object, nat]] ] 
     #]

% if we initialize A and D maps to be predicates, then we should assume something about 
% a starting world state.

  Dom(w: preWS): set[[object, nat]] = { t:[object, nat] | w`ob(t`1) }
 
  WS: TYPE = 
      { w: preWS | FORALL (o1, o2: (w`ob)), (r: (w`r)): 
	              subset?(w`A(o1, r), Dom(w)) AND subset?(w`D(o1,r,o2), Dom(w))
}

  r_e: right


END world_state