diff -r 7f58a9a843c2 -r a462d5207aa6 src/HOL/Boogie/Examples/Boogie_Max.certs
--- a/src/HOL/Boogie/Examples/Boogie_Max.certs	Tue Oct 26 11:45:12 2010 +0200
+++ b/src/HOL/Boogie/Examples/Boogie_Max.certs	Tue Oct 26 11:46:19 2010 +0200
@@ -1,4 +1,4 @@
-3e8da1e086888bc525192984192051f1e39c6752 2224 0
+16ee32e23503be38842c16c90807e66120a960ee 2224 0
 #2 := false
 #8 := 0::int
 decl f5 :: (-> int int)