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 right names in MePo exporter
authorblanchet
Thu, 06 Dec 2012 16:07:09 +0100
changeset 50402 923f1e199f4f
parent 50401 8e5d7ef3da76
child 50403 87868964733c
child 50411 c9023d78d1a6
use right names in MePo exporter
src/HOL/TPTP/MaSh_Eval.thy file | annotate | diff | comparison | revisions
src/HOL/TPTP/mash_export.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/TPTP/MaSh_Eval.thy	Thu Dec 06 15:54:17 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Thu Dec 06 16:07:09 2012 +0100
@@ -11,7 +11,7 @@
 ML_file "mash_eval.ML"
 
 sledgehammer_params
-  [provers = spass, max_relevant = 40, strict, dont_slice, type_enc = mono_native,
+  [provers = spass, max_relevant = 32, strict, dont_slice, type_enc = mono_native,
    lam_trans = combs_and_lifting, timeout = 15, dont_preplay, minimize]
 
 declare [[sledgehammer_instantiate_inducts]]
--- a/src/HOL/TPTP/mash_export.ML	Thu Dec 06 15:54:17 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Thu Dec 06 16:07:09 2012 +0100
@@ -189,7 +189,7 @@
                 old_facts
                 |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
                        max_relevant NONE hyp_ts concl_t
-                |> map (fn ((name, _), _) => name ())
+                |> map (nickname_of o snd)
               val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"
             in File.append path s end
           else
isabelle