--- 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) =>