Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
changeset 39366 f58fbb959826
parent 39339 9608a5bd5d20
child 39452 70a57e40f795 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Sep 14 16:33:38 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Sep 14 16:34:26 2010 +0200
@@ -61,7 +61,7 @@
     val {context = ctxt, goal, ...} = Proof.goal state
     val problem =
       {state = state, goal = goal, subgoal = subgoal,
-       axioms = map (prepare_axiom ctxt) axioms}
+       axioms = map (prepare_axiom ctxt) axioms, only = true}
     val result as {outcome, used_thm_names, ...} = prover params (K "") problem
   in
     priority (case outcome of
isabelle