--- a/src/HOL/Decision_Procs/Cooper.thy Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Fri Dec 02 14:54:25 2011 +0100
@@ -1943,8 +1943,8 @@
term_of_num vs (@{code C} i) $ term_of_num vs t2
| term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
-fun term_of_fm ps vs @{code T} = HOLogic.true_const
- | term_of_fm ps vs @{code F} = HOLogic.false_const
+fun term_of_fm ps vs @{code T} = @{term True}
+ | term_of_fm ps vs @{code F} = @{term False}
| term_of_fm ps vs (@{code Lt} t) =
@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"}
| term_of_fm ps vs (@{code Le} t) =