--- a/src/HOL/TLA/Stfun.thy Mon Feb 10 17:23:13 2014 +0100
+++ b/src/HOL/TLA/Stfun.thy Mon Feb 10 21:00:56 2014 +0100
@@ -10,8 +10,7 @@
begin
typedecl state
-
-arities state :: world
+instance state :: world ..
type_synonym 'a stfun = "state => 'a"
type_synonym stpred = "bool stfun"