src/HOL/IMP/Astate.thy

--- a/src/HOL/IMP/Astate.thy	Tue Sep 13 07:13:49 2011 +0200
+++ b/src/HOL/IMP/Astate.thy	Wed Sep 14 06:49:01 2011 +0200
@@ -30,9 +30,9 @@
 
 definition
 "join_astate F G =
- FunDom (%x. fun F x \<squnion> fun G x) ([x\<leftarrow>dom F. x : set(dom G)])"
+ FunDom (\<lambda>x. fun F x \<squnion> fun G x) ([x\<leftarrow>dom F. x : set(dom G)])"
 
-definition "Top = FunDom (%x. Top) []"
+definition "Top = FunDom (\<lambda>x. Top) []"
 
 instance
 proof