src/HOL/Tools/res_atp.ML
changeset 24920 2a45e400fdad
parent 24867 e5b55d7be9bb
child 24958 ff15f76741bd
     1.1 --- a/src/HOL/Tools/res_atp.ML	Mon Oct 08 22:06:32 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Oct 09 00:20:13 2007 +0200
     1.3 @@ -960,8 +960,7 @@
     1.4      val thy = ProofContext.theory_of ctxt;
     1.5    in
     1.6      Output.debug (fn () => "subgoals in isar_atp:\n" ^
     1.7 -                  Pretty.string_of (ProofContext.pretty_term ctxt
     1.8 -                    (Logic.mk_conjunction_list (Thm.prems_of goal))));
     1.9 +                  Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)));
    1.10      Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
    1.11      app (fn th => Output.debug (fn _ => "chained: " ^ string_of_thm th)) chain_ths;
    1.12      if !time_limit > 0 then isar_atp (ctxt, chain_ths, goal)