diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/record.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -1392,7 +1392,7 @@
              val prop =
                list_all ([("r", T)],
                  Logic.mk_equals
-                  (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), HOLogic.true_const));
+                  (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
             in SOME (prove prop) end
             handle TERM _ => NONE)
         | _ => NONE)
@@ -1644,10 +1644,10 @@
     val inject_prop =  (* FIXME local x x' *)
       let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
         HOLogic.mk_conj (HOLogic.eq_const extT $
-          mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const)
+          mk_ext vars_more $ mk_ext vars_more', @{term True})
         ===
         foldr1 HOLogic.mk_conj
-          (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [HOLogic.true_const])
+          (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [@{term True}])
       end;
 
     val induct_prop =