diff -r 39acf19e9f3a -r 30e2ffbba718 src/HOL/Import/import.ML
--- a/src/HOL/Import/import.ML	Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Import/import.ML	Tue Jul 21 01:03:18 2009 +0200
@@ -44,9 +44,9 @@
             val thm = equal_elim rew thm
             val prew = ProofKernel.rewrite_hol4_term prem thy
             val prem' = #2 (Logic.dest_equals (prop_of prew))
-            val _ = message ("Import proved " ^ Display.string_of_thm thm)
+            val _ = message ("Import proved " ^ Display.string_of_thm ctxt thm)
             val thm = ProofKernel.disambiguate_frees thm
-            val _ = message ("Disambiguate: " ^ Display.string_of_thm thm)
+            val _ = message ("Disambiguate: " ^ Display.string_of_thm ctxt thm)
         in
             case Shuffler.set_prop thy prem' [("",thm)] of
                 SOME (_,thm) =>