proper context for print_tac;
authorwenzelm
Wed Apr 09 12:22:57 2014 +0200 (2014-04-09)
changeset 56491a8ccf3d6a6e4
parent 56490 16d00478b518
child 56492 29a1d14b944c
proper context for print_tac;
src/Doc/Implementation/Tactic.thy
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Probability/measurable.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/Pure/tactical.ML
src/Sequents/prover.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/Doc/Implementation/Tactic.thy	Wed Apr 09 11:32:41 2014 +0200
     1.2 +++ b/src/Doc/Implementation/Tactic.thy	Wed Apr 09 12:22:57 2014 +0200
     1.3 @@ -175,7 +175,7 @@
     1.4    @{index_ML_type tactic: "thm -> thm Seq.seq"} \\
     1.5    @{index_ML no_tac: tactic} \\
     1.6    @{index_ML all_tac: tactic} \\
     1.7 -  @{index_ML print_tac: "string -> tactic"} \\[1ex]
     1.8 +  @{index_ML print_tac: "Proof.context -> string -> tactic"} \\[1ex]
     1.9    @{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]
    1.10    @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\
    1.11    @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\
    1.12 @@ -200,7 +200,7 @@
    1.13    \item @{ML all_tac} is a tactic that always succeeds, returning a
    1.14    singleton sequence with unchanged goal state.
    1.15  
    1.16 -  \item @{ML print_tac}~@{text "message"} is like @{ML all_tac}, but
    1.17 +  \item @{ML print_tac}~@{text "ctxt message"} is like @{ML all_tac}, but
    1.18    prints a message together with the goal state on the tracing
    1.19    channel.
    1.20  
     2.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Wed Apr 09 11:32:41 2014 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Apr 09 12:22:57 2014 +0200
     2.3 @@ -81,9 +81,9 @@
     2.4  val weak_congs   = [@{thm "if_weak_cong"}]
     2.5  
     2.6  (* debugging *)
     2.7 -fun DEBUG_tac (msg,tac) = 
     2.8 -    CHANGED (EVERY [print_tac ("before "^msg), tac, print_tac ("after "^msg)]); 
     2.9 -fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
    2.10 +fun DEBUG_tac ctxt (msg,tac) = 
    2.11 +    CHANGED (EVERY [print_tac ctxt ("before "^msg), tac, print_tac ctxt ("after "^msg)]); 
    2.12 +fun NO_DEBUG_tac _ (_,tac) = CHANGED tac; 
    2.13  
    2.14  
    2.15  (* simproc that deals with instances of permutations in front *)
    2.16 @@ -170,8 +170,8 @@
    2.17  
    2.18  
    2.19  (* main simplification tactics for permutations *)
    2.20 -fun perm_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical (perm_simp stac ctxt i));
    2.21 -fun eqvt_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical (eqvt_simp stac ctxt i)); 
    2.22 +fun perm_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (perm_simp stac ctxt i));
    2.23 +fun eqvt_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (eqvt_simp stac ctxt i)); 
    2.24  
    2.25  val perm_simp_tac_i          = perm_simp_tac_gen_i simp_tac
    2.26  val perm_asm_simp_tac_i      = perm_simp_tac_gen_i asm_simp_tac
    2.27 @@ -253,12 +253,12 @@
    2.28    let fun perm_extend_simp_tac_aux tactical ctxt n = 
    2.29            if n=0 then K all_tac
    2.30            else DETERM o 
    2.31 -               (FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i),
    2.32 -                       fn i => tactical (perm_simp asm_full_simp_tac ctxt i),
    2.33 -                       fn i => tactical (perm_compose_tac ctxt i),
    2.34 -                       fn i => tactical (apply_cong_tac i), 
    2.35 -                       fn i => tactical (unfold_perm_fun_def_tac i),
    2.36 -                       fn i => tactical (ext_fun_tac i)]
    2.37 +               (FIRST'[fn i => tactical ctxt ("splitting conjunctions on the rhs", rtac conjI i),
    2.38 +                       fn i => tactical ctxt (perm_simp asm_full_simp_tac ctxt i),
    2.39 +                       fn i => tactical ctxt (perm_compose_tac ctxt i),
    2.40 +                       fn i => tactical ctxt (apply_cong_tac i), 
    2.41 +                       fn i => tactical ctxt (unfold_perm_fun_def_tac i),
    2.42 +                       fn i => tactical ctxt (ext_fun_tac i)]
    2.43                        THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ctxt (n-1))))
    2.44    in perm_extend_simp_tac_aux tactical ctxt 10 end;
    2.45  
    2.46 @@ -270,11 +270,11 @@
    2.47    let 
    2.48       val simps        = [supports_def, Thm.symmetric fresh_def, fresh_prod]
    2.49    in
    2.50 -      EVERY [tactical ("unfolding of supports   ", simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) i),
    2.51 -             tactical ("stripping of foralls    ", REPEAT_DETERM (rtac allI i)),
    2.52 -             tactical ("geting rid of the imps  ", rtac impI i),
    2.53 -             tactical ("eliminating conjuncts   ", REPEAT_DETERM (etac  conjE i)),
    2.54 -             tactical ("applying eqvt_simp      ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ctxt i )]
    2.55 +      EVERY [tactical ctxt ("unfolding of supports   ", simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) i),
    2.56 +             tactical ctxt ("stripping of foralls    ", REPEAT_DETERM (rtac allI i)),
    2.57 +             tactical ctxt ("geting rid of the imps  ", rtac impI i),
    2.58 +             tactical ctxt ("eliminating conjuncts   ", REPEAT_DETERM (etac  conjE i)),
    2.59 +             tactical ctxt ("applying eqvt_simp      ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ctxt i )]
    2.60    end;
    2.61  
    2.62  
    2.63 @@ -314,7 +314,7 @@
    2.64              val fin_supp = dynamic_thms st ("fin_supp")
    2.65              val ctxt' = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
    2.66            in
    2.67 -            (tactical ("guessing of the right supports-set",
    2.68 +            (tactical ctxt ("guessing of the right supports-set",
    2.69                        EVERY [compose_tac (false, supports_rule'', 2) i,
    2.70                               asm_full_simp_tac ctxt' (i+1),
    2.71                               supports_tac_i tactical ctxt i])) st
    2.72 @@ -356,7 +356,7 @@
    2.73              val supports_fresh_rule'' = Drule.cterm_instantiate
    2.74                [(cert (head_of S), cert s')] supports_fresh_rule'
    2.75            in
    2.76 -            (tactical ("guessing of the right set that supports the goal", 
    2.77 +            (tactical ctxt ("guessing of the right set that supports the goal", 
    2.78                        (EVERY [compose_tac (false, supports_fresh_rule'', 3) i,
    2.79                               asm_full_simp_tac ctxt1 (i+2),
    2.80                               asm_full_simp_tac ctxt2 (i+1), 
    2.81 @@ -364,7 +364,7 @@
    2.82            end
    2.83            (* when a term-constructor contains more than one binder, it is useful    *) 
    2.84            (* in nominal_primrecs to try whether the goal can be solved by an hammer *)
    2.85 -        | _ => (tactical ("if it is not of the form _\<sharp>_, then try the simplifier",   
    2.86 +        | _ => (tactical ctxt ("if it is not of the form _\<sharp>_, then try the simplifier",   
    2.87                            (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps [fresh_prod]@fresh_atm) i))) st
    2.88      end
    2.89      handle General.Subscript => Seq.empty;
     3.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Wed Apr 09 11:32:41 2014 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Wed Apr 09 12:22:57 2014 +0200
     3.3 @@ -47,7 +47,7 @@
     3.4  
     3.5  fun tactic ctxt (msg, tac) =
     3.6    if Config.get ctxt nominal_eqvt_debug
     3.7 -  then tac THEN' (K (print_tac ("after " ^ msg)))
     3.8 +  then tac THEN' (K (print_tac ctxt ("after " ^ msg)))
     3.9    else tac
    3.10  
    3.11  fun prove_eqvt_tac ctxt orig_thm pi pi' =
     4.1 --- a/src/HOL/Probability/measurable.ML	Wed Apr 09 11:32:41 2014 +0200
     4.2 +++ b/src/HOL/Probability/measurable.ML	Wed Apr 09 12:22:57 2014 +0200
     4.3 @@ -95,7 +95,7 @@
     4.4  
     4.5  fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
     4.6  
     4.7 -fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac (msg ()) THEN f else f
     4.8 +fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f
     4.9  
    4.10  fun nth_hol_goal thm i =
    4.11    HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Wed Apr 09 11:32:41 2014 +0200
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Wed Apr 09 12:22:57 2014 +0200
     5.3 @@ -25,11 +25,11 @@
     5.4  
     5.5  (* debug stuff *)
     5.6  
     5.7 -fun trace_tac options s =
     5.8 -  if show_proof_trace options then print_tac s else Seq.single;
     5.9 +fun trace_tac ctxt options s =
    5.10 +  if show_proof_trace options then print_tac ctxt s else Seq.single;
    5.11  
    5.12 -fun assert_tac pos pred =
    5.13 -  COND pred all_tac (print_tac ("Assertion failed" ^ Position.here pos) THEN no_tac);
    5.14 +fun assert_tac ctxt pos pred =
    5.15 +  COND pred all_tac (print_tac ctxt ("Assertion failed" ^ Position.here pos) THEN no_tac);
    5.16  
    5.17  
    5.18  (** special setup for simpset **)
    5.19 @@ -75,9 +75,9 @@
    5.20        | Abs _ => raise Fail "prove_param: No valid parameter term")
    5.21    in
    5.22      REPEAT_DETERM (rtac @{thm ext} 1)
    5.23 -    THEN trace_tac options "prove_param"
    5.24 +    THEN trace_tac ctxt options "prove_param"
    5.25      THEN f_tac
    5.26 -    THEN trace_tac options "after prove_param"
    5.27 +    THEN trace_tac ctxt options "after prove_param"
    5.28      THEN (REPEAT_DETERM (atac 1))
    5.29      THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
    5.30      THEN REPEAT_DETERM (rtac @{thm refl} 1)
    5.31 @@ -92,19 +92,19 @@
    5.32          val param_derivations = param_derivations_of deriv
    5.33          val ho_args = ho_args_of mode args
    5.34        in
    5.35 -        trace_tac options "before intro rule:"
    5.36 +        trace_tac ctxt options "before intro rule:"
    5.37          THEN rtac introrule 1
    5.38 -        THEN trace_tac options "after intro rule"
    5.39 +        THEN trace_tac ctxt options "after intro rule"
    5.40          (* for the right assumption in first position *)
    5.41          THEN rotate_tac premposition 1
    5.42          THEN atac 1
    5.43 -        THEN trace_tac options "parameter goal"
    5.44 +        THEN trace_tac ctxt options "parameter goal"
    5.45          (* work with parameter arguments *)
    5.46          THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
    5.47          THEN (REPEAT_DETERM (atac 1))
    5.48        end
    5.49    | (Free _, _) =>
    5.50 -      trace_tac options "proving parameter call.."
    5.51 +      trace_tac ctxt options "proving parameter call.."
    5.52        THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, concl, ...} =>
    5.53            let
    5.54              val param_prem = nth prems premposition
    5.55 @@ -120,7 +120,7 @@
    5.56            in
    5.57              rtac param_prem' 1
    5.58            end) ctxt 1
    5.59 -      THEN trace_tac options "after prove parameter call")
    5.60 +      THEN trace_tac ctxt options "after prove parameter call")
    5.61  
    5.62  fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st
    5.63  
    5.64 @@ -142,13 +142,13 @@
    5.65    in
    5.66      (* make this simpset better! *)
    5.67      asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps simprules) 1
    5.68 -    THEN trace_tac options "after prove_match:"
    5.69 +    THEN trace_tac ctxt options "after prove_match:"
    5.70      THEN (DETERM (TRY
    5.71             (rtac eval_if_P 1
    5.72             THEN (SUBPROOF (fn {prems, ...} =>
    5.73               (REPEAT_DETERM (rtac @{thm conjI} 1
    5.74               THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1))))
    5.75 -             THEN trace_tac options "if condition to be solved:"
    5.76 +             THEN trace_tac ctxt options "if condition to be solved:"
    5.77               THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
    5.78               THEN TRY (
    5.79                  let
    5.80 @@ -158,8 +158,8 @@
    5.81                      (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
    5.82                  end
    5.83               THEN REPEAT_DETERM (rtac @{thm refl} 1))
    5.84 -             THEN trace_tac options "after if simp; in SUBPROOF") ctxt 1))))
    5.85 -    THEN trace_tac options "after if simplification"
    5.86 +             THEN trace_tac ctxt options "after if simp; in SUBPROOF") ctxt 1))))
    5.87 +    THEN trace_tac ctxt options "after if simplification"
    5.88    end;
    5.89  
    5.90  
    5.91 @@ -189,9 +189,9 @@
    5.92      val (in_ts, clause_out_ts) = split_mode mode ts;
    5.93      fun prove_prems out_ts [] =
    5.94          (prove_match options ctxt nargs out_ts)
    5.95 -        THEN trace_tac options "before simplifying assumptions"
    5.96 +        THEN trace_tac ctxt options "before simplifying assumptions"
    5.97          THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
    5.98 -        THEN trace_tac options "before single intro rule"
    5.99 +        THEN trace_tac ctxt options "before single intro rule"
   5.100          THEN Subgoal.FOCUS_PREMS
   5.101             (fn {context = ctxt', prems, ...} =>
   5.102              let
   5.103 @@ -212,11 +212,11 @@
   5.104                  val (_, out_ts''') = split_mode mode us
   5.105                  val rec_tac = prove_prems out_ts''' ps
   5.106                in
   5.107 -                trace_tac options "before clause:"
   5.108 +                trace_tac ctxt options "before clause:"
   5.109                  (*THEN asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1*)
   5.110 -                THEN trace_tac options "before prove_expr:"
   5.111 +                THEN trace_tac ctxt options "before prove_expr:"
   5.112                  THEN prove_expr options ctxt nargs premposition (t, deriv)
   5.113 -                THEN trace_tac options "after prove_expr:"
   5.114 +                THEN trace_tac ctxt options "after prove_expr:"
   5.115                  THEN rec_tac
   5.116                end
   5.117              | Negprem t =>
   5.118 @@ -231,16 +231,16 @@
   5.119                  val param_derivations = param_derivations_of deriv
   5.120                  val params = ho_args_of mode args
   5.121                in
   5.122 -                trace_tac options "before prove_neg_expr:"
   5.123 +                trace_tac ctxt options "before prove_neg_expr:"
   5.124                  THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
   5.125                    [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
   5.126                     @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
   5.127                  THEN (if (is_some name) then
   5.128 -                    trace_tac options "before applying not introduction rule"
   5.129 +                    trace_tac ctxt options "before applying not introduction rule"
   5.130                      THEN Subgoal.FOCUS_PREMS (fn {prems, ...} =>
   5.131                        rtac (the neg_intro_rule) 1
   5.132                        THEN rtac (nth prems premposition) 1) ctxt 1
   5.133 -                    THEN trace_tac options "after applying not introduction rule"
   5.134 +                    THEN trace_tac ctxt options "after applying not introduction rule"
   5.135                      THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
   5.136                      THEN (REPEAT_DETERM (atac 1))
   5.137                    else
   5.138 @@ -255,16 +255,16 @@
   5.139                end
   5.140              | Sidecond t =>
   5.141               rtac @{thm if_predI} 1
   5.142 -             THEN trace_tac options "before sidecond:"
   5.143 +             THEN trace_tac ctxt options "before sidecond:"
   5.144               THEN prove_sidecond ctxt t
   5.145 -             THEN trace_tac options "after sidecond:"
   5.146 +             THEN trace_tac ctxt options "after sidecond:"
   5.147               THEN prove_prems [] ps)
   5.148          in (prove_match options ctxt nargs out_ts)
   5.149              THEN rest_tac
   5.150          end
   5.151      val prems_tac = prove_prems in_ts moded_ps
   5.152    in
   5.153 -    trace_tac options "Proving clause..."
   5.154 +    trace_tac ctxt options "Proving clause..."
   5.155      THEN rtac @{thm bindI} 1
   5.156      THEN rtac @{thm singleI} 1
   5.157      THEN prems_tac
   5.158 @@ -281,15 +281,15 @@
   5.159      val pred_case_rule = the_elim_of ctxt pred
   5.160    in
   5.161      REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))
   5.162 -    THEN trace_tac options "before applying elim rule"
   5.163 +    THEN trace_tac ctxt options "before applying elim rule"
   5.164      THEN etac (predfun_elim_of ctxt pred mode) 1
   5.165      THEN etac pred_case_rule 1
   5.166 -    THEN trace_tac options "after applying elim rule"
   5.167 +    THEN trace_tac ctxt options "after applying elim rule"
   5.168      THEN (EVERY (map
   5.169             (fn i => EVERY' (select_sup (length moded_clauses) i) i)
   5.170               (1 upto (length moded_clauses))))
   5.171      THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses))
   5.172 -    THEN trace_tac options "proved one direction"
   5.173 +    THEN trace_tac ctxt options "proved one direction"
   5.174    end
   5.175  
   5.176  
   5.177 @@ -306,15 +306,15 @@
   5.178              val num_of_constrs = length case_thms
   5.179              val (_, ts) = strip_comb t
   5.180            in
   5.181 -            trace_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^
   5.182 +            trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^
   5.183                " splitting with rules \n" ^ Display.string_of_thm ctxt split_asm)
   5.184              THEN TRY (Splitter.split_asm_tac [split_asm] 1
   5.185 -              THEN (trace_tac options "after splitting with split_asm rules")
   5.186 +              THEN (trace_tac ctxt options "after splitting with split_asm rules")
   5.187              (* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1)
   5.188                THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
   5.189                THEN (REPEAT_DETERM_N (num_of_constrs - 1)
   5.190                  (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
   5.191 -            THEN assert_tac @{here} (fn st => Thm.nprems_of st <= 2)
   5.192 +            THEN assert_tac ctxt @{here} (fn st => Thm.nprems_of st <= 2)
   5.193              THEN (EVERY (map split_term_tac ts))
   5.194            end
   5.195        else all_tac
   5.196 @@ -343,9 +343,9 @@
   5.197        | Free _ => all_tac
   5.198        | _ => error "prove_param2: illegal parameter term")
   5.199    in
   5.200 -    trace_tac options "before simplification in prove_args:"
   5.201 +    trace_tac ctxt options "before simplification in prove_args:"
   5.202      THEN f_tac
   5.203 -    THEN trace_tac options "after simplification in prove_args"
   5.204 +    THEN trace_tac ctxt options "after simplification in prove_args"
   5.205      THEN EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)
   5.206    end
   5.207  
   5.208 @@ -359,11 +359,11 @@
   5.209          in
   5.210            etac @{thm bindE} 1
   5.211            THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
   5.212 -          THEN trace_tac options "prove_expr2-before"
   5.213 +          THEN trace_tac ctxt options "prove_expr2-before"
   5.214            THEN etac (predfun_elim_of ctxt name mode) 1
   5.215 -          THEN trace_tac options "prove_expr2"
   5.216 +          THEN trace_tac ctxt options "prove_expr2"
   5.217            THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
   5.218 -          THEN trace_tac options "finished prove_expr2"
   5.219 +          THEN trace_tac ctxt options "finished prove_expr2"
   5.220          end
   5.221        | _ => etac @{thm bindE} 1)
   5.222  
   5.223 @@ -384,7 +384,7 @@
   5.224      (* only simplify the one assumption *)
   5.225      full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1
   5.226      (* need better control here! *)
   5.227 -    THEN trace_tac options "after sidecond2 simplification"
   5.228 +    THEN trace_tac ctxt options "after sidecond2 simplification"
   5.229    end
   5.230  
   5.231  fun prove_clause2 options ctxt pred mode (ts, ps) i =
   5.232 @@ -396,9 +396,9 @@
   5.233        addsimps [@{thm split_eta}, @{thm split_beta},
   5.234          @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
   5.235      fun prove_prems2 out_ts [] =
   5.236 -      trace_tac options "before prove_match2 - last call:"
   5.237 +      trace_tac ctxt options "before prove_match2 - last call:"
   5.238        THEN prove_match2 options ctxt out_ts
   5.239 -      THEN trace_tac options "after prove_match2 - last call:"
   5.240 +      THEN trace_tac ctxt options "after prove_match2 - last call:"
   5.241        THEN (etac @{thm singleE} 1)
   5.242        THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
   5.243        THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1)
   5.244 @@ -406,13 +406,13 @@
   5.245          (REPEAT_DETERM (etac @{thm Pair_inject} 1))
   5.246          THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1)
   5.247  
   5.248 -        THEN SOLVED (trace_tac options "state before applying intro rule:"
   5.249 +        THEN SOLVED (trace_tac ctxt options "state before applying intro rule:"
   5.250          THEN (rtac pred_intro_rule
   5.251          (* How to handle equality correctly? *)
   5.252 -        THEN_ALL_NEW (K (trace_tac options "state before assumption matching")
   5.253 +        THEN_ALL_NEW (K (trace_tac ctxt options "state before assumption matching")
   5.254          THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_simpset) THEN' (TRY o atac)))
   5.255 -          THEN' (K (trace_tac options "state after pre-simplification:"))
   5.256 -        THEN' (K (trace_tac options "state after assumption matching:")))) 1))
   5.257 +          THEN' (K (trace_tac ctxt options "state after pre-simplification:"))
   5.258 +        THEN' (K (trace_tac ctxt options "state after assumption matching:")))) 1))
   5.259      | prove_prems2 out_ts ((p, deriv) :: ps) =
   5.260        let
   5.261          val mode = head_mode_of deriv
   5.262 @@ -435,7 +435,7 @@
   5.263                  val param_derivations = param_derivations_of deriv
   5.264                  val ho_args = ho_args_of mode args
   5.265                in
   5.266 -                trace_tac options "before neg prem 2"
   5.267 +                trace_tac ctxt options "before neg prem 2"
   5.268                  THEN etac @{thm bindE} 1
   5.269                  THEN (if is_some name then
   5.270                      full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
   5.271 @@ -453,18 +453,18 @@
   5.272                THEN prove_sidecond2 options ctxt t
   5.273                THEN prove_prems2 [] ps)
   5.274        in
   5.275 -        trace_tac options "before prove_match2:"
   5.276 +        trace_tac ctxt options "before prove_match2:"
   5.277          THEN prove_match2 options ctxt out_ts
   5.278 -        THEN trace_tac options "after prove_match2:"
   5.279 +        THEN trace_tac ctxt options "after prove_match2:"
   5.280          THEN rest_tac
   5.281        end
   5.282      val prems_tac = prove_prems2 in_ts ps
   5.283    in
   5.284 -    trace_tac options "starting prove_clause2"
   5.285 +    trace_tac ctxt options "starting prove_clause2"
   5.286      THEN etac @{thm bindE} 1
   5.287      THEN (etac @{thm singleE'} 1)
   5.288      THEN (TRY (etac @{thm Pair_inject} 1))
   5.289 -    THEN trace_tac options "after singleE':"
   5.290 +    THEN trace_tac ctxt options "after singleE':"
   5.291      THEN prems_tac
   5.292    end;
   5.293  
   5.294 @@ -495,11 +495,11 @@
   5.295        (if not (skip_proof options) then
   5.296          (fn _ =>
   5.297          rtac @{thm pred_iffI} 1
   5.298 -        THEN trace_tac options "after pred_iffI"
   5.299 +        THEN trace_tac ctxt options "after pred_iffI"
   5.300          THEN prove_one_direction options ctxt clauses preds pred mode moded_clauses
   5.301 -        THEN trace_tac options "proved one direction"
   5.302 +        THEN trace_tac ctxt options "proved one direction"
   5.303          THEN prove_other_direction options ctxt pred mode moded_clauses
   5.304 -        THEN trace_tac options "proved other direction")
   5.305 +        THEN trace_tac ctxt options "proved other direction")
   5.306        else (fn _ => ALLGOALS Skip_Proof.cheat_tac))
   5.307    end
   5.308  
     6.1 --- a/src/Pure/tactical.ML	Wed Apr 09 11:32:41 2014 +0200
     6.2 +++ b/src/Pure/tactical.ML	Wed Apr 09 12:22:57 2014 +0200
     6.3 @@ -30,7 +30,7 @@
     6.4    val FIRST': ('a -> tactic) list -> 'a -> tactic
     6.5    val FIRST1: (int -> tactic) list -> tactic
     6.6    val RANGE: (int -> tactic) list -> int -> tactic
     6.7 -  val print_tac: string -> tactic
     6.8 +  val print_tac: Proof.context -> string -> tactic
     6.9    val pause_tac: tactic
    6.10    val trace_REPEAT: bool Unsynchronized.ref
    6.11    val suppress_tracing: bool Unsynchronized.ref
    6.12 @@ -182,9 +182,8 @@
    6.13  (*** Tracing tactics ***)
    6.14  
    6.15  (*Print the current proof state and pass it on.*)
    6.16 -fun print_tac msg st =
    6.17 - (tracing (msg ^ "\n" ^
    6.18 -    Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals_without_context st)));
    6.19 +fun print_tac ctxt msg st =
    6.20 + (tracing (msg ^ "\n" ^ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals ctxt st)));
    6.21    Seq.single st);
    6.22  
    6.23  (*Pause until a line is typed -- if non-empty then fail. *)
     7.1 --- a/src/Sequents/prover.ML	Wed Apr 09 11:32:41 2014 +0200
     7.2 +++ b/src/Sequents/prover.ML	Wed Apr 09 12:22:57 2014 +0200
     7.3 @@ -196,7 +196,7 @@
     7.4      val lastrestac = RESOLVE_THEN unsafes;
     7.5      fun gtac i =
     7.6        restac gtac i ORELSE
     7.7 -       (if Config.get ctxt trace then print_tac "" THEN lastrestac gtac i
     7.8 +       (if Config.get ctxt trace then print_tac ctxt "" THEN lastrestac gtac i
     7.9          else lastrestac gtac i)
    7.10    in gtac end;
    7.11  
     8.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Apr 09 11:32:41 2014 +0200
     8.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Apr 09 12:22:57 2014 +0200
     8.3 @@ -226,13 +226,13 @@
     8.4       rewrite_goals_tac ctxt con_defs,
     8.5       REPEAT (rtac @{thm refl} 2),
     8.6       (*Typechecking; this can fail*)
     8.7 -     if !Ind_Syntax.trace then print_tac "The type-checking subgoal:"
     8.8 +     if !Ind_Syntax.trace then print_tac ctxt "The type-checking subgoal:"
     8.9       else all_tac,
    8.10       REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
    8.11                          ORELSE' eresolve_tac (asm_rl :: @{thm PartE} :: @{thm SigmaE2} ::
    8.12                                                type_elims)
    8.13                          ORELSE' hyp_subst_tac ctxt1)),
    8.14 -     if !Ind_Syntax.trace then print_tac "The subgoal after monos, type_elims:"
    8.15 +     if !Ind_Syntax.trace then print_tac ctxt "The subgoal after monos, type_elims:"
    8.16       else all_tac,
    8.17       DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
    8.18