diff -r 799b687e4aac -r 32effb2a8168 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Thu Feb 26 06:21:31 2009 -0800
+++ b/src/HOL/Decision_Procs/MIR.thy	Thu Feb 26 06:33:48 2009 -0800
@@ -5926,7 +5926,7 @@
 apply mir
 done
 
-lemma "ALL x y. \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
+lemma "ALL (x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
 apply mir
 done