--- a/src/HOL/TLA/Stfun.thy Sat Dec 01 18:51:46 2001 +0100 +++ b/src/HOL/TLA/Stfun.thy Sat Dec 01 18:52:32 2001 +0100 @@ -17,7 +17,7 @@ stpred = "bool stfun" arities - state :: term + state :: type instance state :: world