--- a/src/HOL/TPTP/mash_export.ML Thu Jan 17 23:29:17 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML Thu Jan 17 23:29:22 2013 +0100
@@ -213,10 +213,10 @@
let
val (name, mash_suggs) =
extract_suggestions mash_line
- ||> (map fst #> weight_mash_facts)
+ ||> weight_mash_facts
val (name', mepo_suggs) =
extract_suggestions mepo_line
- ||> (map fst #> weight_mash_facts)
+ ||> weight_mepo_facts
val _ = if name = name' then () else error "Input files out of sync."
val mess =
[(mepo_weight, (mepo_suggs, [])),