src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 35592 768d17f54125
parent 35569 77dfdbf85fb8
child 35826 1590abc3d42a
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Mar 05 23:31:58 2010 +0100
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Mar 05 23:51:32 2010 +0100
     1.3 @@ -253,7 +253,7 @@
     1.4      NONE => warning ("Unknown external prover: " ^ quote name)
     1.5    | SOME prover =>
     1.6        let
     1.7 -        val {context = ctxt, facts, goal} = Proof.raw_goal proof_state; (* FIXME Proof.goal *)
     1.8 +        val {context = ctxt, facts, goal} = Proof.goal proof_state;
     1.9          val desc =
    1.10            "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
    1.11              Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));