--- a/src/HOL/TLA/Init.thy Tue Feb 23 10:11:15 2010 +0100 +++ b/src/HOL/TLA/Init.thy Tue Feb 23 10:11:16 2010 +0100 @@ -12,7 +12,7 @@ begin typedecl behavior -instance behavior :: world .. +arities behavior :: world types temporal = "behavior form"