1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Wed Oct 28 22:04:57 2009 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Wed Oct 28 22:18:00 2009 +0100
     1.3 @@ -151,11 +151,11 @@
     1.4  
     1.5  (* Mirabelle utility functions *)
     1.6  
     1.7 -val goal_thm_of = snd o snd o Proof.get_goal
     1.8 +val goal_thm_of = #goal o Proof.raw_goal  (* FIXME ?? *)
     1.9  
    1.10  fun can_apply time tac st =
    1.11    let
    1.12 -    val (ctxt, (facts, goal)) = Proof.get_goal st
    1.13 +    val {context = ctxt, facts, goal} = Proof.raw_goal st   (* FIXME ?? *)
    1.14      val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
    1.15    in
    1.16      (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of

     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Oct 28 22:04:57 2009 +0100
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Oct 28 22:18:00 2009 +0100
     2.3 @@ -301,13 +301,13 @@
     2.4  
     2.5  fun run_sh prover hard_timeout timeout dir st =
     2.6    let
     2.7 -    val (ctxt, goal) = Proof.get_goal st
     2.8 +    val {context = ctxt, facts, goal} = Proof.raw_goal st   (* FIXME ?? *)
     2.9      val change_dir = (fn SOME d => Config.put ATP_Wrapper.destdir d | _ => I)
    2.10      val ctxt' =
    2.11        ctxt
    2.12        |> change_dir dir
    2.13        |> Config.put ATP_Wrapper.measure_runtime true
    2.14 -    val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', goal);
    2.15 +    val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
    2.16  
    2.17      val time_limit =
    2.18        (case hard_timeout of
    2.19 @@ -424,7 +424,7 @@
    2.20    end
    2.21  
    2.22  fun sledgehammer_action args id (st as {log, pre, name, ...}: Mirabelle.run_args) =
    2.23 -  let val goal = Thm.major_prem_of(snd(snd(Proof.get_goal pre))) in
    2.24 +  let val goal = Thm.major_prem_of (#goal (Proof.raw_goal pre))  (* FIXME ?? *) in
    2.25    if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
    2.26    then () else
    2.27    let

     3.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Oct 28 22:04:57 2009 +0100
     3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Oct 28 22:18:00 2009 +0100
     3.3 @@ -254,7 +254,7 @@
     3.4      NONE => warning ("Unknown external prover: " ^ quote name)
     3.5    | SOME prover =>
     3.6        let
     3.7 -        val full_goal as (ctxt, (_, goal)) = Proof.get_goal proof_state;
     3.8 +        val {context = ctxt, facts, goal} = Proof.raw_goal proof_state; (* FIXME Proof.goal *)
     3.9          val desc =
    3.10            "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
    3.11              Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
    3.12 @@ -262,7 +262,7 @@
    3.13          val _ = SimpleThread.fork true (fn () =>
    3.14            let
    3.15              val _ = register birth_time death_time (Thread.self (), desc);
    3.16 -            val problem = ATP_Wrapper.problem_of_goal (! full_types) i full_goal;
    3.17 +            val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
    3.18              val result =
    3.19                let val {success, message, ...} = prover (! timeout) problem;
    3.20                in (success, message) end

     4.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Oct 28 22:04:57 2009 +0100
     4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Oct 28 22:18:00 2009 +0100
     4.3 @@ -104,10 +104,11 @@
     4.4      val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
     4.5      val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
     4.6      val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
     4.7 +    val {context = ctxt, facts, goal} = Proof.raw_goal state   (* FIXME ?? *)
     4.8      val problem =
     4.9       {with_full_types = ! ATP_Manager.full_types,
    4.10        subgoal = subgoalno,
    4.11 -      goal = Proof.get_goal state,
    4.12 +      goal = (ctxt, (facts, goal)),
    4.13        axiom_clauses = SOME axclauses,
    4.14        filtered_clauses = filtered}
    4.15      val (result, proof) = produce_answer (prover time_limit problem)

     5.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Oct 28 22:04:57 2009 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Oct 28 22:18:00 2009 +0100
     5.3 @@ -854,7 +854,7 @@
     5.4  fun pick_nits_in_subgoal state params auto subgoal =
     5.5    let
     5.6      val ctxt = Proof.context_of state
     5.7 -    val t = state |> Proof.get_goal |> snd |> snd |> prop_of
     5.8 +    val t = state |> Proof.raw_goal |> #goal |> prop_of
     5.9    in
    5.10      if Logic.count_prems t = 0 then
    5.11        (priority "No subgoal!"; ("none", state))

     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Oct 28 22:04:57 2009 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Oct 28 22:18:00 2009 +0100
     6.3 @@ -417,7 +417,7 @@
     6.4    let
     6.5      val thy = Proof.theory_of state
     6.6      val ctxt = Proof.context_of state
     6.7 -    val thm = snd (snd (Proof.get_goal state))
     6.8 +    val thm = #goal (Proof.raw_goal state)
     6.9      val _ = List.app check_raw_param override_params
    6.10      val params as {blocking, debug, ...} =
    6.11        extract_params ctxt auto (default_raw_params thy) override_params