diff -r ad3a8569759c -r 2a45e400fdad src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -960,8 +960,7 @@
     val thy = ProofContext.theory_of ctxt;
   in
     Output.debug (fn () => "subgoals in isar_atp:\n" ^
-                  Pretty.string_of (ProofContext.pretty_term ctxt
-                    (Logic.mk_conjunction_list (Thm.prems_of goal))));
+                  Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)));
     Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
     app (fn th => Output.debug (fn _ => "chained: " ^ string_of_thm th)) chain_ths;
     if !time_limit > 0 then isar_atp (ctxt, chain_ths, goal)