equal
deleted
inserted
replaced
958 let |
958 let |
959 val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state); |
959 val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state); |
960 val thy = ProofContext.theory_of ctxt; |
960 val thy = ProofContext.theory_of ctxt; |
961 in |
961 in |
962 Output.debug (fn () => "subgoals in isar_atp:\n" ^ |
962 Output.debug (fn () => "subgoals in isar_atp:\n" ^ |
963 Pretty.string_of (ProofContext.pretty_term ctxt |
963 Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal))); |
964 (Logic.mk_conjunction_list (Thm.prems_of goal)))); |
|
965 Output.debug (fn () => "current theory: " ^ Context.theory_name thy); |
964 Output.debug (fn () => "current theory: " ^ Context.theory_name thy); |
966 app (fn th => Output.debug (fn _ => "chained: " ^ string_of_thm th)) chain_ths; |
965 app (fn th => Output.debug (fn _ => "chained: " ^ string_of_thm th)) chain_ths; |
967 if !time_limit > 0 then isar_atp (ctxt, chain_ths, goal) |
966 if !time_limit > 0 then isar_atp (ctxt, chain_ths, goal) |
968 else (warning ("Writing problem file only: " ^ !problem_name); |
967 else (warning ("Writing problem file only: " ^ !problem_name); |
969 isar_atp_writeonly (ctxt, chain_ths, goal)) |
968 isar_atp_writeonly (ctxt, chain_ths, goal)) |