diff -r d68b705719ce -r 6b780867d426 src/ZF/UNITY/State.thy --- a/src/ZF/UNITY/State.thy Wed Dec 30 17:38:57 2015 +0100 +++ b/src/ZF/UNITY/State.thy Wed Dec 30 17:45:18 2015 +0100 @@ -21,7 +21,7 @@ default_val :: "i=>i" definition - "state == \ x \ var. cons(default_val(x), type_of(x))" + "state == \x \ var. cons(default_val(x), type_of(x))" definition "st0 == \x \ var. default_val(x)"