# HG changeset patch
# User blanchet
# Date 1358337329 -3600
# Node ID a86708897266a90bfc1f7f6acb6f19d04cbdb938
# Parent  67b04a8375b034435b513be81286a8c96d033d34
graceful failure

diff -r 67b04a8375b0 -r a86708897266 src/HOL/TPTP/mash_export.ML
--- 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;