added tracing to ATP exporter
authorblanchet
Sun Dec 16 12:07:37 2012 +0100 (2012-12-16)
changeset 505619a733bd6c0ba
parent 50560 e4dc37ec1427
child 50562 0a7c7e121bd8
added tracing to ATP exporter
src/HOL/TPTP/mash_export.ML
     1.1 --- a/src/HOL/TPTP/mash_export.ML	Sat Dec 15 22:19:14 2012 +0100
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Sun Dec 16 12:07:37 2012 +0100
     1.3 @@ -123,6 +123,7 @@
     1.4        if in_range range j then
     1.5          let
     1.6            val name = nickname_of th
     1.7 +          val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
     1.8            val deps =
     1.9              isar_or_prover_dependencies_of ctxt params_opt facts all_names th
    1.10                                             NONE
    1.11 @@ -153,6 +154,7 @@
    1.12      fun do_fact (j, ((name, ((_, stature), th)), prevs)) =
    1.13        if in_range range j then
    1.14          let
    1.15 +          val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
    1.16            val feats =
    1.17              features_of ctxt prover (theory_of_thm th) stature [prop_of th]
    1.18            val isar_deps = isar_dependencies_of all_names th