diff -r 39acf19e9f3a -r 30e2ffbba718 src/HOL/Tools/atp_wrapper.ML
--- a/src/HOL/Tools/atp_wrapper.ML	Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML	Tue Jul 21 01:03:18 2009 +0200
@@ -62,7 +62,7 @@
     val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno)
       handle THM ("assume: variables", _, _) =>
         error "Sledgehammer: Goal contains type variables (TVars)"
-    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls
+    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm ctxt th)) goal_cls
     val the_filtered_clauses =
       case filtered_clauses of
           NONE => relevance_filter goal goal_cls