# HG changeset patch
# User wenzelm
# Date 894615339 -7200
# Node ID 5f6b2dd1cd11d601211c0e257ac5f1ebc5d2802f
# Parent  0f56199a8d97fd2dc5de8bb0a642a06b7f23384e
fixed update syntax;

diff -r 0f56199a8d97 -r 5f6b2dd1cd11 src/HOLCF/IMP/Denotational.thy
--- a/src/HOLCF/IMP/Denotational.thy	Thu May 07 18:34:48 1998 +0200
+++ b/src/HOLCF/IMP/Denotational.thy	Fri May 08 10:15:39 1998 +0200
@@ -16,7 +16,7 @@
 
 primrec D com
   "D(SKIP) = (LAM s. Def(undiscr s))"
-  "D(X := a) = (LAM s. Def((undiscr s)[a(undiscr s)/X]))"
+  "D(X := a) = (LAM s. Def((undiscr s)[X := a(undiscr s)]))"
   "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
   "D(IF b THEN c1 ELSE c2) =
 	(LAM s. if b(undiscr s) then (D c1)`s else (D c2)`s)"