--- a/src/HOL/TPTP/mash_export.ML Wed Jan 16 12:46:11 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML Wed Jan 16 12:55:29 2013 +0100
@@ -223,6 +223,11 @@
in File.append mesh_path mesh_line end
val mash_lines = Path.explode mash_file_name |> File.read_lines
val mepo_lines = Path.explode mepo_file_name |> File.read_lines
- in List.app do_fact (mash_lines ~~ mepo_lines) end
+ in
+ if length mash_lines = length mepo_lines then
+ List.app do_fact (mash_lines ~~ mepo_lines)
+ else
+ warning "Skipped: MaSh file missing or out of sync with MePo file."
+ end
end;