# HG changeset patch # User wenzelm # Date 1397038977 -7200 # Node ID a8ccf3d6a6e4a6324759be0f0d5ed3863190af07 # Parent 16d00478b518fa2a8a332eef3196026d65ae7a44 proper context for print_tac; diff -r 16d00478b518 -r a8ccf3d6a6e4 src/Doc/Implementation/Tactic.thy --- a/src/Doc/Implementation/Tactic.thy Wed Apr 09 11:32:41 2014 +0200 +++ b/src/Doc/Implementation/Tactic.thy Wed Apr 09 12:22:57 2014 +0200 @@ -175,7 +175,7 @@ @{index_ML_type tactic: "thm -> thm Seq.seq"} \\ @{index_ML no_tac: tactic} \\ @{index_ML all_tac: tactic} \\ - @{index_ML print_tac: "string -> tactic"} \\[1ex] + @{index_ML print_tac: "Proof.context -> string -> tactic"} \\[1ex] @{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex] @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\ @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\ @@ -200,7 +200,7 @@ \item @{ML all_tac} is a tactic that always succeeds, returning a singleton sequence with unchanged goal state. - \item @{ML print_tac}~@{text "message"} is like @{ML all_tac}, but + \item @{ML print_tac}~@{text "ctxt message"} is like @{ML all_tac}, but prints a message together with the goal state on the tracing channel. diff -r 16d00478b518 -r a8ccf3d6a6e4 src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Wed Apr 09 11:32:41 2014 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Wed Apr 09 12:22:57 2014 +0200 @@ -81,9 +81,9 @@ val weak_congs = [@{thm "if_weak_cong"}] (* debugging *) -fun DEBUG_tac (msg,tac) = - CHANGED (EVERY [print_tac ("before "^msg), tac, print_tac ("after "^msg)]); -fun NO_DEBUG_tac (_,tac) = CHANGED tac; +fun DEBUG_tac ctxt (msg,tac) = + CHANGED (EVERY [print_tac ctxt ("before "^msg), tac, print_tac ctxt ("after "^msg)]); +fun NO_DEBUG_tac _ (_,tac) = CHANGED tac; (* simproc that deals with instances of permutations in front *) @@ -170,8 +170,8 @@ (* main simplification tactics for permutations *) -fun perm_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical (perm_simp stac ctxt i)); -fun eqvt_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical (eqvt_simp stac ctxt i)); +fun perm_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (perm_simp stac ctxt i)); +fun eqvt_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (eqvt_simp stac ctxt i)); val perm_simp_tac_i = perm_simp_tac_gen_i simp_tac val perm_asm_simp_tac_i = perm_simp_tac_gen_i asm_simp_tac @@ -253,12 +253,12 @@ let fun perm_extend_simp_tac_aux tactical ctxt n = if n=0 then K all_tac else DETERM o - (FIRST'[fn i => tactical ("splitting conjunctions on the rhs", rtac conjI i), - fn i => tactical (perm_simp asm_full_simp_tac ctxt i), - fn i => tactical (perm_compose_tac ctxt i), - fn i => tactical (apply_cong_tac i), - fn i => tactical (unfold_perm_fun_def_tac i), - fn i => tactical (ext_fun_tac i)] + (FIRST'[fn i => tactical ctxt ("splitting conjunctions on the rhs", rtac conjI i), + fn i => tactical ctxt (perm_simp asm_full_simp_tac ctxt i), + fn i => tactical ctxt (perm_compose_tac ctxt i), + fn i => tactical ctxt (apply_cong_tac i), + fn i => tactical ctxt (unfold_perm_fun_def_tac i), + fn i => tactical ctxt (ext_fun_tac i)] THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ctxt (n-1)))) in perm_extend_simp_tac_aux tactical ctxt 10 end; @@ -270,11 +270,11 @@ let val simps = [supports_def, Thm.symmetric fresh_def, fresh_prod] in - EVERY [tactical ("unfolding of supports ", simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) i), - tactical ("stripping of foralls ", REPEAT_DETERM (rtac allI i)), - tactical ("geting rid of the imps ", rtac impI i), - tactical ("eliminating conjuncts ", REPEAT_DETERM (etac conjE i)), - tactical ("applying eqvt_simp ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ctxt i )] + EVERY [tactical ctxt ("unfolding of supports ", simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) i), + tactical ctxt ("stripping of foralls ", REPEAT_DETERM (rtac allI i)), + tactical ctxt ("geting rid of the imps ", rtac impI i), + tactical ctxt ("eliminating conjuncts ", REPEAT_DETERM (etac conjE i)), + tactical ctxt ("applying eqvt_simp ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ctxt i )] end; @@ -314,7 +314,7 @@ val fin_supp = dynamic_thms st ("fin_supp") val ctxt' = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp in - (tactical ("guessing of the right supports-set", + (tactical ctxt ("guessing of the right supports-set", EVERY [compose_tac (false, supports_rule'', 2) i, asm_full_simp_tac ctxt' (i+1), supports_tac_i tactical ctxt i])) st @@ -356,7 +356,7 @@ val supports_fresh_rule'' = Drule.cterm_instantiate [(cert (head_of S), cert s')] supports_fresh_rule' in - (tactical ("guessing of the right set that supports the goal", + (tactical ctxt ("guessing of the right set that supports the goal", (EVERY [compose_tac (false, supports_fresh_rule'', 3) i, asm_full_simp_tac ctxt1 (i+2), asm_full_simp_tac ctxt2 (i+1), @@ -364,7 +364,7 @@ end (* when a term-constructor contains more than one binder, it is useful *) (* in nominal_primrecs to try whether the goal can be solved by an hammer *) - | _ => (tactical ("if it is not of the form _\_, then try the simplifier", + | _ => (tactical ctxt ("if it is not of the form _\_, then try the simplifier", (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps [fresh_prod]@fresh_atm) i))) st end handle General.Subscript => Seq.empty; diff -r 16d00478b518 -r a8ccf3d6a6e4 src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Wed Apr 09 11:32:41 2014 +0200 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Wed Apr 09 12:22:57 2014 +0200 @@ -47,7 +47,7 @@ fun tactic ctxt (msg, tac) = if Config.get ctxt nominal_eqvt_debug - then tac THEN' (K (print_tac ("after " ^ msg))) + then tac THEN' (K (print_tac ctxt ("after " ^ msg))) else tac fun prove_eqvt_tac ctxt orig_thm pi pi' = diff -r 16d00478b518 -r a8ccf3d6a6e4 src/HOL/Probability/measurable.ML --- a/src/HOL/Probability/measurable.ML Wed Apr 09 11:32:41 2014 +0200 +++ b/src/HOL/Probability/measurable.ML Wed Apr 09 12:22:57 2014 +0200 @@ -95,7 +95,7 @@ fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt; -fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac (msg ()) THEN f else f +fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f fun nth_hol_goal thm i = HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1)))) diff -r 16d00478b518 -r a8ccf3d6a6e4 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Apr 09 11:32:41 2014 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Apr 09 12:22:57 2014 +0200 @@ -25,11 +25,11 @@ (* debug stuff *) -fun trace_tac options s = - if show_proof_trace options then print_tac s else Seq.single; +fun trace_tac ctxt options s = + if show_proof_trace options then print_tac ctxt s else Seq.single; -fun assert_tac pos pred = - COND pred all_tac (print_tac ("Assertion failed" ^ Position.here pos) THEN no_tac); +fun assert_tac ctxt pos pred = + COND pred all_tac (print_tac ctxt ("Assertion failed" ^ Position.here pos) THEN no_tac); (** special setup for simpset **) @@ -75,9 +75,9 @@ | Abs _ => raise Fail "prove_param: No valid parameter term") in REPEAT_DETERM (rtac @{thm ext} 1) - THEN trace_tac options "prove_param" + THEN trace_tac ctxt options "prove_param" THEN f_tac - THEN trace_tac options "after prove_param" + THEN trace_tac ctxt options "after prove_param" THEN (REPEAT_DETERM (atac 1)) THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations)) THEN REPEAT_DETERM (rtac @{thm refl} 1) @@ -92,19 +92,19 @@ val param_derivations = param_derivations_of deriv val ho_args = ho_args_of mode args in - trace_tac options "before intro rule:" + trace_tac ctxt options "before intro rule:" THEN rtac introrule 1 - THEN trace_tac options "after intro rule" + THEN trace_tac ctxt options "after intro rule" (* for the right assumption in first position *) THEN rotate_tac premposition 1 THEN atac 1 - THEN trace_tac options "parameter goal" + THEN trace_tac ctxt options "parameter goal" (* work with parameter arguments *) THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations)) THEN (REPEAT_DETERM (atac 1)) end | (Free _, _) => - trace_tac options "proving parameter call.." + trace_tac ctxt options "proving parameter call.." THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, concl, ...} => let val param_prem = nth prems premposition @@ -120,7 +120,7 @@ in rtac param_prem' 1 end) ctxt 1 - THEN trace_tac options "after prove parameter call") + THEN trace_tac ctxt options "after prove parameter call") fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st @@ -142,13 +142,13 @@ in (* make this simpset better! *) asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps simprules) 1 - THEN trace_tac options "after prove_match:" + THEN trace_tac ctxt options "after prove_match:" THEN (DETERM (TRY (rtac eval_if_P 1 THEN (SUBPROOF (fn {prems, ...} => (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1)))) - THEN trace_tac options "if condition to be solved:" + THEN trace_tac ctxt options "if condition to be solved:" THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1 THEN TRY ( let @@ -158,8 +158,8 @@ (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 end THEN REPEAT_DETERM (rtac @{thm refl} 1)) - THEN trace_tac options "after if simp; in SUBPROOF") ctxt 1)))) - THEN trace_tac options "after if simplification" + THEN trace_tac ctxt options "after if simp; in SUBPROOF") ctxt 1)))) + THEN trace_tac ctxt options "after if simplification" end; @@ -189,9 +189,9 @@ val (in_ts, clause_out_ts) = split_mode mode ts; fun prove_prems out_ts [] = (prove_match options ctxt nargs out_ts) - THEN trace_tac options "before simplifying assumptions" + THEN trace_tac ctxt options "before simplifying assumptions" THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1 - THEN trace_tac options "before single intro rule" + THEN trace_tac ctxt options "before single intro rule" THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, ...} => let @@ -212,11 +212,11 @@ val (_, out_ts''') = split_mode mode us val rec_tac = prove_prems out_ts''' ps in - trace_tac options "before clause:" + trace_tac ctxt options "before clause:" (*THEN asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1*) - THEN trace_tac options "before prove_expr:" + THEN trace_tac ctxt options "before prove_expr:" THEN prove_expr options ctxt nargs premposition (t, deriv) - THEN trace_tac options "after prove_expr:" + THEN trace_tac ctxt options "after prove_expr:" THEN rec_tac end | Negprem t => @@ -231,16 +231,16 @@ val param_derivations = param_derivations_of deriv val params = ho_args_of mode args in - trace_tac options "before prove_neg_expr:" + trace_tac ctxt options "before prove_neg_expr:" THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1 THEN (if (is_some name) then - trace_tac options "before applying not introduction rule" + trace_tac ctxt options "before applying not introduction rule" THEN Subgoal.FOCUS_PREMS (fn {prems, ...} => rtac (the neg_intro_rule) 1 THEN rtac (nth prems premposition) 1) ctxt 1 - THEN trace_tac options "after applying not introduction rule" + THEN trace_tac ctxt options "after applying not introduction rule" THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations)) THEN (REPEAT_DETERM (atac 1)) else @@ -255,16 +255,16 @@ end | Sidecond t => rtac @{thm if_predI} 1 - THEN trace_tac options "before sidecond:" + THEN trace_tac ctxt options "before sidecond:" THEN prove_sidecond ctxt t - THEN trace_tac options "after sidecond:" + THEN trace_tac ctxt options "after sidecond:" THEN prove_prems [] ps) in (prove_match options ctxt nargs out_ts) THEN rest_tac end val prems_tac = prove_prems in_ts moded_ps in - trace_tac options "Proving clause..." + trace_tac ctxt options "Proving clause..." THEN rtac @{thm bindI} 1 THEN rtac @{thm singleI} 1 THEN prems_tac @@ -281,15 +281,15 @@ val pred_case_rule = the_elim_of ctxt pred in REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})) - THEN trace_tac options "before applying elim rule" + THEN trace_tac ctxt options "before applying elim rule" THEN etac (predfun_elim_of ctxt pred mode) 1 THEN etac pred_case_rule 1 - THEN trace_tac options "after applying elim rule" + THEN trace_tac ctxt options "after applying elim rule" THEN (EVERY (map (fn i => EVERY' (select_sup (length moded_clauses) i) i) (1 upto (length moded_clauses)))) THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses)) - THEN trace_tac options "proved one direction" + THEN trace_tac ctxt options "proved one direction" end @@ -306,15 +306,15 @@ val num_of_constrs = length case_thms val (_, ts) = strip_comb t in - trace_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^ + trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^ " splitting with rules \n" ^ Display.string_of_thm ctxt split_asm) THEN TRY (Splitter.split_asm_tac [split_asm] 1 - THEN (trace_tac options "after splitting with split_asm rules") + THEN (trace_tac ctxt options "after splitting with split_asm rules") (* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1) THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*) THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2))) - THEN assert_tac @{here} (fn st => Thm.nprems_of st <= 2) + THEN assert_tac ctxt @{here} (fn st => Thm.nprems_of st <= 2) THEN (EVERY (map split_term_tac ts)) end else all_tac @@ -343,9 +343,9 @@ | Free _ => all_tac | _ => error "prove_param2: illegal parameter term") in - trace_tac options "before simplification in prove_args:" + trace_tac ctxt options "before simplification in prove_args:" THEN f_tac - THEN trace_tac options "after simplification in prove_args" + THEN trace_tac ctxt options "after simplification in prove_args" THEN EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations) end @@ -359,11 +359,11 @@ in etac @{thm bindE} 1 THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))) - THEN trace_tac options "prove_expr2-before" + THEN trace_tac ctxt options "prove_expr2-before" THEN etac (predfun_elim_of ctxt name mode) 1 - THEN trace_tac options "prove_expr2" + THEN trace_tac ctxt options "prove_expr2" THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)) - THEN trace_tac options "finished prove_expr2" + THEN trace_tac ctxt options "finished prove_expr2" end | _ => etac @{thm bindE} 1) @@ -384,7 +384,7 @@ (* only simplify the one assumption *) full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1 (* need better control here! *) - THEN trace_tac options "after sidecond2 simplification" + THEN trace_tac ctxt options "after sidecond2 simplification" end fun prove_clause2 options ctxt pred mode (ts, ps) i = @@ -396,9 +396,9 @@ addsimps [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] fun prove_prems2 out_ts [] = - trace_tac options "before prove_match2 - last call:" + trace_tac ctxt options "before prove_match2 - last call:" THEN prove_match2 options ctxt out_ts - THEN trace_tac options "after prove_match2 - last call:" + THEN trace_tac ctxt options "after prove_match2 - last call:" THEN (etac @{thm singleE} 1) THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1)) THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1) @@ -406,13 +406,13 @@ (REPEAT_DETERM (etac @{thm Pair_inject} 1)) THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1) - THEN SOLVED (trace_tac options "state before applying intro rule:" + THEN SOLVED (trace_tac ctxt options "state before applying intro rule:" THEN (rtac pred_intro_rule (* How to handle equality correctly? *) - THEN_ALL_NEW (K (trace_tac options "state before assumption matching") + THEN_ALL_NEW (K (trace_tac ctxt options "state before assumption matching") THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_simpset) THEN' (TRY o atac))) - THEN' (K (trace_tac options "state after pre-simplification:")) - THEN' (K (trace_tac options "state after assumption matching:")))) 1)) + THEN' (K (trace_tac ctxt options "state after pre-simplification:")) + THEN' (K (trace_tac ctxt options "state after assumption matching:")))) 1)) | prove_prems2 out_ts ((p, deriv) :: ps) = let val mode = head_mode_of deriv @@ -435,7 +435,7 @@ val param_derivations = param_derivations_of deriv val ho_args = ho_args_of mode args in - trace_tac options "before neg prem 2" + trace_tac ctxt options "before neg prem 2" THEN etac @{thm bindE} 1 THEN (if is_some name then full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @@ -453,18 +453,18 @@ THEN prove_sidecond2 options ctxt t THEN prove_prems2 [] ps) in - trace_tac options "before prove_match2:" + trace_tac ctxt options "before prove_match2:" THEN prove_match2 options ctxt out_ts - THEN trace_tac options "after prove_match2:" + THEN trace_tac ctxt options "after prove_match2:" THEN rest_tac end val prems_tac = prove_prems2 in_ts ps in - trace_tac options "starting prove_clause2" + trace_tac ctxt options "starting prove_clause2" THEN etac @{thm bindE} 1 THEN (etac @{thm singleE'} 1) THEN (TRY (etac @{thm Pair_inject} 1)) - THEN trace_tac options "after singleE':" + THEN trace_tac ctxt options "after singleE':" THEN prems_tac end; @@ -495,11 +495,11 @@ (if not (skip_proof options) then (fn _ => rtac @{thm pred_iffI} 1 - THEN trace_tac options "after pred_iffI" + THEN trace_tac ctxt options "after pred_iffI" THEN prove_one_direction options ctxt clauses preds pred mode moded_clauses - THEN trace_tac options "proved one direction" + THEN trace_tac ctxt options "proved one direction" THEN prove_other_direction options ctxt pred mode moded_clauses - THEN trace_tac options "proved other direction") + THEN trace_tac ctxt options "proved other direction") else (fn _ => ALLGOALS Skip_Proof.cheat_tac)) end diff -r 16d00478b518 -r a8ccf3d6a6e4 src/Pure/tactical.ML --- a/src/Pure/tactical.ML Wed Apr 09 11:32:41 2014 +0200 +++ b/src/Pure/tactical.ML Wed Apr 09 12:22:57 2014 +0200 @@ -30,7 +30,7 @@ val FIRST': ('a -> tactic) list -> 'a -> tactic val FIRST1: (int -> tactic) list -> tactic val RANGE: (int -> tactic) list -> int -> tactic - val print_tac: string -> tactic + val print_tac: Proof.context -> string -> tactic val pause_tac: tactic val trace_REPEAT: bool Unsynchronized.ref val suppress_tracing: bool Unsynchronized.ref @@ -182,9 +182,8 @@ (*** Tracing tactics ***) (*Print the current proof state and pass it on.*) -fun print_tac msg st = - (tracing (msg ^ "\n" ^ - Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals_without_context st))); +fun print_tac ctxt msg st = + (tracing (msg ^ "\n" ^ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals ctxt st))); Seq.single st); (*Pause until a line is typed -- if non-empty then fail. *) diff -r 16d00478b518 -r a8ccf3d6a6e4 src/Sequents/prover.ML --- a/src/Sequents/prover.ML Wed Apr 09 11:32:41 2014 +0200 +++ b/src/Sequents/prover.ML Wed Apr 09 12:22:57 2014 +0200 @@ -196,7 +196,7 @@ val lastrestac = RESOLVE_THEN unsafes; fun gtac i = restac gtac i ORELSE - (if Config.get ctxt trace then print_tac "" THEN lastrestac gtac i + (if Config.get ctxt trace then print_tac ctxt "" THEN lastrestac gtac i else lastrestac gtac i) in gtac end; diff -r 16d00478b518 -r a8ccf3d6a6e4 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Wed Apr 09 11:32:41 2014 +0200 +++ b/src/ZF/Tools/inductive_package.ML Wed Apr 09 12:22:57 2014 +0200 @@ -226,13 +226,13 @@ rewrite_goals_tac ctxt con_defs, REPEAT (rtac @{thm refl} 2), (*Typechecking; this can fail*) - if !Ind_Syntax.trace then print_tac "The type-checking subgoal:" + if !Ind_Syntax.trace then print_tac ctxt "The type-checking subgoal:" else all_tac, REPEAT (FIRSTGOAL ( dresolve_tac rec_typechecks ORELSE' eresolve_tac (asm_rl :: @{thm PartE} :: @{thm SigmaE2} :: type_elims) ORELSE' hyp_subst_tac ctxt1)), - if !Ind_Syntax.trace then print_tac "The subgoal after monos, type_elims:" + if !Ind_Syntax.trace then print_tac ctxt "The subgoal after monos, type_elims:" else all_tac, DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];