src/HOL/Hoare/Hoare.thy

--- a/src/HOL/Hoare/Hoare.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Hoare/Hoare.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -34,7 +34,7 @@
   "Skip s s' == (s=s')"
 
   Assign        :: [pvar, 'a exp] => 'a com
-  "Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
+  "Assign v e s s' == (s' = (%x. if x=v then e(s) else s(x)))"
 
   Seq           :: ['a com, 'a com] => 'a com
   "Seq c c' s s' == ? s''. c s s'' & c' s'' s'"