--- 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