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/TPTP/mash_export.ML
changeset 48406 b002cc16aa99
parent 48404 0a261b4aa093
child 48438 3e45c98fe127 
--- a/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -179,7 +179,7 @@
             let
               val suggs =
                 old_facts
-                |> Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
+                |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
                        max_relevant NONE hyp_ts concl_t
                 |> map (fn ((name, _), _) => name ())
               val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"
isabelle