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.
compile
authorblanchet
Mon, 28 Jun 2010 11:04:02 +0200
changeset 37587 466031e057a0
parent 37586 a209fff74792
child 37588 030dfe572619
compile
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 28 08:55:46 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 28 11:04:02 2010 +0200
@@ -393,7 +393,8 @@
       |> the_default 5
     val params = default_params thy
       [("atps", prover_name), ("minimize_timeout", Int.toString timeout)]
-    val minimize = minimize_theorems params 1 (subgoal_count st)
+    val minimize =
+      Sledgehammer_Fact_Minimizer.minimize_theorems params 1 (subgoal_count st)
     val _ = log separator
   in
     case minimize st (these (!named_thms)) of
isabelle