# HG changeset patch
# User blanchet
# Date 1355656057 -3600
# Node ID 9a733bd6c0ba0b155cdf394f84b041e86d942426
# Parent  e4dc37ec14273050942622ddd862bf45997e1826
added tracing to ATP exporter

diff -r e4dc37ec1427 -r 9a733bd6c0ba src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Sat Dec 15 22:19:14 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Sun Dec 16 12:07:37 2012 +0100
@@ -123,6 +123,7 @@
       if in_range range j then
         let
           val name = nickname_of th
+          val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
           val deps =
             isar_or_prover_dependencies_of ctxt params_opt facts all_names th
                                            NONE
@@ -153,6 +154,7 @@
     fun do_fact (j, ((name, ((_, stature), th)), prevs)) =
       if in_range range j then
         let
+          val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
           val feats =
             features_of ctxt prover (theory_of_thm th) stature [prop_of th]
           val isar_deps = isar_dependencies_of all_names th