# HG changeset patch
# User blanchet
# Date 1354806429 -3600
# Node ID 923f1e199f4f6ac68075d1f2d08fe106ebfc3609
# Parent  8e5d7ef3da7610d14cae3d1aca43f8ec892b144d
use right names in MePo exporter

diff -r 8e5d7ef3da76 -r 923f1e199f4f src/HOL/TPTP/MaSh_Eval.thy
--- 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]]
diff -r 8e5d7ef3da76 -r 923f1e199f4f src/HOL/TPTP/mash_export.ML
--- 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