--- a/Derivatives.thy	Tue Jul 26 10:58:26 2011 +0000
+++ b/Derivatives.thy	Tue Jul 26 18:12:07 2011 +0000
@@ -115,7 +115,8 @@
 | "der c (One) = Zero"
 | "der c (Atom c') = (if c = c' then One else Zero)"
 | "der c (Plus r1 r2) = Plus (der c r1) (der c r2)"
-| "der c (Times r1 r2) = Plus (Times (der c r1) r2) (if nullable r1 then der c r2 else Zero)"
+| "der c (Times r1 r2) = 
+    (if nullable r1 then Plus (Times (der c r1) r2) (der c r2) else Times (der c r1) r2)"
 | "der c (Star r) = Times (der c r) (Star r)"
 
 function