1.1 --- a/src/HOL/TPTP/mash_export.ML	Thu Jan 17 23:29:17 2013 +0100
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Thu Jan 17 23:29:22 2013 +0100
     1.3 @@ -213,10 +213,10 @@
     1.4        let
     1.5          val (name, mash_suggs) =
     1.6            extract_suggestions mash_line
     1.7 -          ||> (map fst #> weight_mash_facts)
     1.8 +          ||> weight_mash_facts
     1.9          val (name', mepo_suggs) =
    1.10            extract_suggestions mepo_line
    1.11 -          ||> (map fst #> weight_mash_facts)
    1.12 +          ||> weight_mepo_facts
    1.13          val _ = if name = name' then () else error "Input files out of sync."
    1.14          val mess =
    1.15            [(mepo_weight, (mepo_suggs, [])),