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.
tuned comment
authorblanchet
Fri, 13 May 2011 10:10:43 +0200
changeset 42782 39ed2de5997a
parent 42781 4b7a988a0213
child 42783 226962b6a6d1
tuned comment
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 13 10:10:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 13 10:10:43 2011 +0200
@@ -489,7 +489,6 @@
                      |> SMT_Monomorph.monomorph indexed_facts
                      |> fst |> sort (int_ord o pairself fst)
                      |> filter_out (curry (op =) ~1 o fst)
-(* FIXME:            |> take max_mono_instances (* just in case *) *)
                      |> map (Untranslated_Fact o apfst (fst o nth facts))
               end
             fun run_slice blacklist (slice, (time_frac, (complete,
isabelle