# HG changeset patch
# User haftmann
# Date 1412533858 -7200
# Node ID d230e7075bcfe65ab039d35e053407d081e6eeac
# Parent  30cc7ee5ac10e6958456f596fe262c17dff7fef9
code preprocessor tracing also for function transformers

diff -r 30cc7ee5ac10 -r d230e7075bcf src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Oct 05 20:30:57 2014 +0200
+++ b/src/Pure/Isar/code.ML	Sun Oct 05 20:30:58 2014 +0200
@@ -918,9 +918,17 @@
   end;
 
 fun cert_of_eqns_preprocess ctxt functrans c =
-  (perhaps o perhaps_loop o perhaps_apply) functrans
-  #> (map o apfst) (preprocess eqn_conv ctxt)
-  #> cert_of_eqns ctxt c;
+  let
+    fun trace_eqns s eqns = (Pretty.writeln o Pretty.chunks)
+      (Pretty.str s :: map (Display.pretty_thm ctxt o fst) eqns);
+    val tracing = if Config.get ctxt simp_trace then trace_eqns else (K o K) ();
+  in
+    tap (tracing "before function transformation")
+    #> (perhaps o perhaps_loop o perhaps_apply) functrans
+    #> tap (tracing "after function transformation")
+    #> (map o apfst) (preprocess eqn_conv ctxt)
+    #> cert_of_eqns ctxt c
+  end;
 
 fun get_cert ctxt functrans c =
   let