src/HOL/Tools/refute.ML

--- a/src/HOL/Tools/refute.ML	Thu Mar 27 14:41:06 2008 +0100
+++ b/src/HOL/Tools/refute.ML	Thu Mar 27 14:41:07 2008 +0100
@@ -456,7 +456,7 @@
           (* schematic type variable not instantiated *)
           raise REFUTE ("monomorphic_term",
             "no substitution for type variable " ^ fst (fst v) ^
-            " in term " ^ Display.raw_string_of_term t)
+            " in term " ^ Sign.string_of_term CPure.thy t)
         | SOME typ =>
           typ)) t;