updated application of print_tac to take context parameter;
authorsultana
Sun Jun 22 06:16:56 2014 +0100 (2014-06-22)
changeset 577727d9134b032b2
parent 57771 0265ccdb9e6f
child 57773 2719eb9d40fe
updated application of print_tac to take context parameter;
src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sat Aug 02 00:15:08 2014 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sun Jun 22 06:16:56 2014 +0100
     1.3 @@ -249,7 +249,7 @@
     1.4  (*given a list of tactics to be applied in sequence (i.e., they
     1.5    follow a skeleton), we build a single tactic, interleaving
     1.6    some tracing info to help with debugging.*)
     1.7 -fun step_by_step_tacs verbose (thm_tacs : (thm * tactic) list) : tactic =
     1.8 +fun step_by_step_tacs ctxt verbose (thm_tacs : (thm * tactic) list) : tactic =
     1.9      let
    1.10        fun interleave_tacs [] [] = all_tac
    1.11          | interleave_tacs (tac1 :: tacs1) (tac2 :: tacs2) =
    1.12 @@ -258,7 +258,7 @@
    1.13        val thms_to_traceprint =
    1.14          map (fn thm => fn st =>
    1.15                (*FIXME uses makestring*)
    1.16 -              print_tac (PolyML.makestring thm) st)
    1.17 +              print_tac ctxt (PolyML.makestring thm) st)
    1.18  
    1.19      in
    1.20        if verbose then
    1.21 @@ -272,9 +272,9 @@
    1.22  
    1.23  ML {*
    1.24  (*apply step_by_step_tacs to all problems under test*)
    1.25 -val narrated_tactics =
    1.26 +fun narrated_tactics ctxt =
    1.27   map (map (#3 #> the)
    1.28 -      #> step_by_step_tacs false)
    1.29 +      #> step_by_step_tacs ctxt false)
    1.30     the_tactics;
    1.31  
    1.32  (*produce thm*)
    1.33 @@ -284,7 +284,7 @@
    1.34    map (fn (prob_name, tac) =>
    1.35           TPTP_Reconstruct.reconstruct @{context}
    1.36             (fn _ => tac) prob_name)
    1.37 -    (ListPair.zip (prob_names, narrated_tactics))
    1.38 +    (ListPair.zip (prob_names, narrated_tactics @{context}))
    1.39  *}
    1.40  
    1.41