# HG changeset patch
# User wenzelm
# Date 1256764680 -3600
# Node ID affe60b3d8642f2328502679d7df759cccd928b4
# Parent  93f0238151f608bdff7a302c586583d71e018efb
renamed raw Proof.get_goal to Proof.raw_goal;

diff -r 93f0238151f6 -r affe60b3d864 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Wed Oct 28 22:04:57 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Wed Oct 28 22:18:00 2009 +0100
@@ -151,11 +151,11 @@
 
 (* Mirabelle utility functions *)
 
-val goal_thm_of = snd o snd o Proof.get_goal
+val goal_thm_of = #goal o Proof.raw_goal  (* FIXME ?? *)
 
 fun can_apply time tac st =
   let
-    val (ctxt, (facts, goal)) = Proof.get_goal st
+    val {context = ctxt, facts, goal} = Proof.raw_goal st   (* FIXME ?? *)
     val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
   in
     (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of
diff -r 93f0238151f6 -r affe60b3d864 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Oct 28 22:04:57 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Oct 28 22:18:00 2009 +0100
@@ -301,13 +301,13 @@
 
 fun run_sh prover hard_timeout timeout dir st =
   let
-    val (ctxt, goal) = Proof.get_goal st
+    val {context = ctxt, facts, goal} = Proof.raw_goal st   (* FIXME ?? *)
     val change_dir = (fn SOME d => Config.put ATP_Wrapper.destdir d | _ => I)
     val ctxt' =
       ctxt
       |> change_dir dir
       |> Config.put ATP_Wrapper.measure_runtime true
-    val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', goal);
+    val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
 
     val time_limit =
       (case hard_timeout of
@@ -424,7 +424,7 @@
   end
 
 fun sledgehammer_action args id (st as {log, pre, name, ...}: Mirabelle.run_args) =
-  let val goal = Thm.major_prem_of(snd(snd(Proof.get_goal pre))) in
+  let val goal = Thm.major_prem_of (#goal (Proof.raw_goal pre))  (* FIXME ?? *) in
   if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
   then () else
   let
diff -r 93f0238151f6 -r affe60b3d864 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Oct 28 22:04:57 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Oct 28 22:18:00 2009 +0100
@@ -254,7 +254,7 @@
     NONE => warning ("Unknown external prover: " ^ quote name)
   | SOME prover =>
       let
-        val full_goal as (ctxt, (_, goal)) = Proof.get_goal proof_state;
+        val {context = ctxt, facts, goal} = Proof.raw_goal proof_state; (* FIXME Proof.goal *)
         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));
@@ -262,7 +262,7 @@
         val _ = SimpleThread.fork true (fn () =>
           let
             val _ = register birth_time death_time (Thread.self (), desc);
-            val problem = ATP_Wrapper.problem_of_goal (! full_types) i full_goal;
+            val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
             val result =
               let val {success, message, ...} = prover (! timeout) problem;
               in (success, message) end
diff -r 93f0238151f6 -r affe60b3d864 src/HOL/Tools/ATP_Manager/atp_minimal.ML
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Oct 28 22:04:57 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Oct 28 22:18:00 2009 +0100
@@ -104,10 +104,11 @@
     val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
     val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
     val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
+    val {context = ctxt, facts, goal} = Proof.raw_goal state   (* FIXME ?? *)
     val problem =
      {with_full_types = ! ATP_Manager.full_types,
       subgoal = subgoalno,
-      goal = Proof.get_goal state,
+      goal = (ctxt, (facts, goal)),
       axiom_clauses = SOME axclauses,
       filtered_clauses = filtered}
     val (result, proof) = produce_answer (prover time_limit problem)
diff -r 93f0238151f6 -r affe60b3d864 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Oct 28 22:04:57 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Oct 28 22:18:00 2009 +0100
@@ -854,7 +854,7 @@
 fun pick_nits_in_subgoal state params auto subgoal =
   let
     val ctxt = Proof.context_of state
-    val t = state |> Proof.get_goal |> snd |> snd |> prop_of
+    val t = state |> Proof.raw_goal |> #goal |> prop_of
   in
     if Logic.count_prems t = 0 then
       (priority "No subgoal!"; ("none", state))
diff -r 93f0238151f6 -r affe60b3d864 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Oct 28 22:04:57 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Oct 28 22:18:00 2009 +0100
@@ -417,7 +417,7 @@
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
-    val thm = snd (snd (Proof.get_goal state))
+    val thm = #goal (Proof.raw_goal state)
     val _ = List.app check_raw_param override_params
     val params as {blocking, debug, ...} =
       extract_params ctxt auto (default_raw_params thy) override_params