# HG changeset patch
# User desharna
# Date 1632140651 -7200
# Node ID 9d304ef5c9320f64533ac8e53f78a230628aa609
# Parent  d6f1ca21a3c1545a11dc0fe1c4fb698f4ff5b9ab
added offset to Mirabelle's tptp output names

diff -r d6f1ca21a3c1 -r 9d304ef5c932 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Mon Oct 04 10:17:11 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Mon Sep 20 14:24:11 2021 +0200
@@ -347,7 +347,9 @@
     fun set_file_name (SOME dir) =
         Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir
         #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix
-          ("prob_" ^ StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "__")
+          ("prob_" ^
+            StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "_" ^
+            StringCvt.padLeft #"0" 6 (str0 (Position.offset_of pos)) ^ "__")
         #> Config.put SMT_Config.debug_files
           (dir ^ "/" ^ Name.desymbolize (SOME false) (ATP_Util.timestamp ()) ^ "_"
           ^ serial_string ())