# HG changeset patch
# User sultana
# Date 1403414216 -3600
# Node ID 7d9134b032b2ecd70caa07213c68dcc63cf0aa80
# Parent  0265ccdb9e6f9bdca6403b189ecaf034ac572a8f
updated application of print_tac to take context parameter;

diff -r 0265ccdb9e6f -r 7d9134b032b2 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sat Aug 02 00:15:08 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sun Jun 22 06:16:56 2014 +0100
@@ -249,7 +249,7 @@
 (*given a list of tactics to be applied in sequence (i.e., they
   follow a skeleton), we build a single tactic, interleaving
   some tracing info to help with debugging.*)
-fun step_by_step_tacs verbose (thm_tacs : (thm * tactic) list) : tactic =
+fun step_by_step_tacs ctxt verbose (thm_tacs : (thm * tactic) list) : tactic =
     let
       fun interleave_tacs [] [] = all_tac
         | interleave_tacs (tac1 :: tacs1) (tac2 :: tacs2) =
@@ -258,7 +258,7 @@
       val thms_to_traceprint =
         map (fn thm => fn st =>
               (*FIXME uses makestring*)
-              print_tac (PolyML.makestring thm) st)
+              print_tac ctxt (PolyML.makestring thm) st)
 
     in
       if verbose then
@@ -272,9 +272,9 @@
 
 ML {*
 (*apply step_by_step_tacs to all problems under test*)
-val narrated_tactics =
+fun narrated_tactics ctxt =
  map (map (#3 #> the)
-      #> step_by_step_tacs false)
+      #> step_by_step_tacs ctxt false)
    the_tactics;
 
 (*produce thm*)
@@ -284,7 +284,7 @@
   map (fn (prob_name, tac) =>
          TPTP_Reconstruct.reconstruct @{context}
            (fn _ => tac) prob_name)
-    (ListPair.zip (prob_names, narrated_tactics))
+    (ListPair.zip (prob_names, narrated_tactics @{context}))
 *}