--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 05 23:31:58 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 05 23:51:32 2010 +0100
@@ -253,7 +253,7 @@
NONE => warning ("Unknown external prover: " ^ quote name)
| SOME prover =>
let
- val {context = ctxt, facts, goal} = Proof.raw_goal proof_state; (* FIXME Proof.goal *)
+ val {context = ctxt, facts, goal} = Proof.goal proof_state;
val desc =
"external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));