diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Fri Dec 02 14:54:25 2011 +0100
@@ -5602,8 +5602,8 @@
   | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t))
   | term_of_num vs (@{code CF} (c, t, s)) = term_of_num vs (@{code Add} (@{code Mul} (c, @{code Floor} t), s));
 
-fun term_of_fm vs @{code T} = HOLogic.true_const 
-  | term_of_fm vs @{code F} = HOLogic.false_const
+fun term_of_fm vs @{code T} = @{term True} 
+  | term_of_fm vs @{code F} = @{term False}
   | term_of_fm vs (@{code Lt} t) =
       @{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::real"}
   | term_of_fm vs (@{code Le} t) =