--- 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.
--- 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 _\<sharp>_, then try the simplifier",
+ | _ => (tactical ctxt ("if it is not of the form _\<sharp>_, 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;
--- 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' =
--- 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))))
--- 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
--- 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. *)
--- 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;
--- 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)];