diff -r 26c2e053ab96 -r ce8f7944fd6b src/HOL/IMP/Abs_Int_Tests.thy
--- a/src/HOL/IMP/Abs_Int_Tests.thy	Sun Feb 05 16:53:20 2012 +0100
+++ b/src/HOL/IMP/Abs_Int_Tests.thy	Sun Feb 05 17:09:21 2012 +0100
@@ -52,9 +52,9 @@
  DO ''x'' ::= Plus (V ''x'') (N 1)"
 
 definition "test4_ivl =
- ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
+ ''x'' ::= N 0; ''y'' ::= N 0;
  WHILE Less (V ''x'') (N 11)
- DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
+ DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N 1))"
 
 definition "test5_ivl =
  ''x'' ::= N 0; ''y'' ::= N 0;