# HG changeset patch
# User blanchet
# Date 1271778060 -7200
# Node ID 56bf63d70120e1de73ff125daf4fc2eab8b14603
# Parent  86e62a98deea8ac14bd1a5ce1e78506ec891ecdf
use "Proof.goal" in Sledgehammer's minimizer (just like everywhere else in Sledgehammer), not "Proof.raw_goal"

diff -r 86e62a98deea -r 56bf63d70120 src/HOL/Tools/ATP_Manager/atp_minimal.ML
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Tue Apr 20 16:14:45 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Tue Apr 20 17:41:00 2010 +0200
@@ -71,7 +71,7 @@
                       " theorem" ^ plural_s num_theorems ^ "...")
     val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
     val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
-    val {context = ctxt, facts, goal} = Proof.raw_goal state
+    val {context = ctxt, facts, goal} = Proof.goal state
     val problem =
      {subgoal = subgoal, goal = (ctxt, (facts, goal)),
       relevance_override = {add = [], del = [], only = false},