src/HOL/Tools/ATP/atp_reconstruct.ML

--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Fri Dec 02 14:54:25 2011 +0100
@@ -586,7 +586,7 @@
 
 (* No "real" literals means only type information (tfree_tcs, clsrel, or
    clsarity). *)
-val is_only_type_information = curry (op aconv) HOLogic.true_const
+val is_only_type_information = curry (op aconv) @{term True}
 
 fun replace_one_dependency (old, new) dep =
   if is_same_atp_step dep old then new else [dep]