src/HOL/Probability/measurable.ML

     fun IF' c t i = COND (c i) (t i) no_tac
 
     fun r_tac msg =
       if Config.get ctxt debug
       then FIRST' o
-        map (fn thm => resolve_tac [thm]
+        map (fn thm => resolve_tac ctxt [thm]
           THEN' K (debug_tac ctxt (debug_fact (msg ^ " resolved using") thm) all_tac))
-      else resolve_tac
+      else resolve_tac ctxt
 
     val elem_congI = @{lemma "A = B \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A" by simp}
 
     val (thms, ctxt) = prepare_facts ctxt facts
 

       Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
         let
           val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
           fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
           fun inst (ts, Ts) =
-            Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) @{thm measurable_compose_countable}
+            Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts)
+              @{thm measurable_compose_countable}
         in r_tac "split countable" (cnt_prefixes ctxt f |> map inst) i end
         handle TERM _ => no_tac) 1)
 
     val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac