src/HOL/IMP/Com.thy

--- a/src/HOL/IMP/Com.thy	Fri Mar 17 22:46:26 1995 +0100
+++ b/src/HOL/IMP/Com.thy	Mon Mar 20 15:35:28 1995 +0100
@@ -86,7 +86,7 @@
        "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
 
 rules 
-	assign_def	"s[m/x] == (%y. if (y=x) m (s y))"
+	assign_def	"s[m/x] == (%y. if y=x then m else s y)"
 
 inductive "evalc"
   intrs