--- a/src/HOL/IMPP/Com.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/IMPP/Com.thy Sat Dec 01 18:52:32 2001 +0100
@@ -12,7 +12,7 @@
current Isabelle, types cannot be refined later *)
types glb
loc
-arities (*val,*)glb,loc :: term
+arities (*val,*)glb,loc :: type
consts Arg, Res :: loc
datatype vname = Glb glb | Loc loc
@@ -21,14 +21,14 @@
datatype state = st globs locals
(* for the meta theory, the following would be sufficient:
types state
-arities state::term
+arities state::type
consts st:: [globs , locals] => state
*)
types aexp = state => val
bexp = state => bool
types pname
-arities pname :: term
+arities pname :: type
datatype com
= SKIP