repair after bc01725d7918;

--- a/src/HOL/HOLCF/IMP/Denotational.thy	Fri May 17 08:19:52 2013 +0200
+++ b/src/HOL/HOLCF/IMP/Denotational.thy	Fri May 17 11:05:59 2013 +0200
@@ -17,7 +17,7 @@
 where
   "D(SKIP) = (LAM s. Def(undiscr s))"
 | "D(X ::= a) = (LAM s. Def((undiscr s)(X := aval a (undiscr s))))"
-| "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
+| "D(c0 ;; c1) = (dlift(D c1) oo (D c0))"
 | "D(IF b THEN c1 ELSE c2) =
         (LAM s. if bval b (undiscr s) then (D c1)\<cdot>s else (D c2)\<cdot>s)"
 | "D(WHILE b DO c) =