diff -r 378ae9e46175 -r 04448228381d src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Sat Jan 25 21:52:04 2014 +0100
+++ b/src/HOL/Set_Interval.thy	Sat Jan 25 22:06:07 2014 +0100
@@ -728,7 +728,7 @@
 qed auto
 
 lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}"
-by(auto intro!: image_eqI[where x="nat x", standard])
+  by (auto intro!: image_eqI [where x = "nat x" for x])
 
 context ordered_ab_group_add
 begin