Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use "Proof.goal" in Sledgehammer's minimizer (just like everywhere else in Sledgehammer), not "Proof.raw_goal"
authorblanchet
Tue, 20 Apr 2010 17:41:00 +0200
changeset 36263 56bf63d70120
parent 36237 86e62a98deea
child 36264 3c2490917710
use "Proof.goal" in Sledgehammer's minimizer (just like everywhere else in Sledgehammer), not "Proof.raw_goal"
src/HOL/Tools/ATP_Manager/atp_minimal.ML file | annotate | diff | comparison | revisions 
--- 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},
isabelle