generate proper nicks also for instantiated induction rules
authorblanchet
Sun Dec 16 12:07:56 2012 +0100 (2012-12-16)
changeset 505620a7c7e121bd8
parent 50561 9a733bd6c0ba
child 50563 3a4785d64ecb
generate proper nicks also for instantiated induction rules
src/HOL/TPTP/mash_eval.ML
     1.1 --- a/src/HOL/TPTP/mash_eval.ML	Sun Dec 16 12:07:37 2012 +0100
     1.2 +++ b/src/HOL/TPTP/mash_eval.ML	Sun Dec 16 12:07:56 2012 +0100
     1.3 @@ -114,10 +114,9 @@
     1.4                  ((K (nickname_of th), stature), th)
     1.5                val facts =
     1.6                  facts
     1.7 -                |> map get
     1.8 +                |> map (get #> nickify)
     1.9                  |> maybe_instantiate_inducts ctxt hyp_ts concl_t
    1.10                  |> take (the max_facts)
    1.11 -                |> map nickify
    1.12                val ctxt = ctxt |> set_file_name heading prob_dir_name
    1.13                val res as {outcome, ...} =
    1.14                  run_prover_for_mash ctxt params prover facts goal