src/Tools/coherent.ML

 
 
 (** external interface **)
 
 fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context = ctxt', ...} =>
-  resolve_tac [rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2] 1 THEN
+  resolve_tac ctxt' [rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2] 1 THEN
   SUBPROOF (fn {prems = prems', concl, context = ctxt'', ...} =>
     let
       val xs =
         map (term_of o #2) params @
         map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s)))

     in
       (case
         valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
           (mk_dom xs) Net.empty 0 0 of
         NONE => no_tac
-      | SOME prf => resolve_tac [thm_of_cl_prf ctxt'' concl [] prf] 1)
+      | SOME prf => resolve_tac ctxt'' [thm_of_cl_prf ctxt'' concl [] prf] 1)
     end) ctxt' 1) ctxt;
 
 val _ = Theory.setup
   (trace_setup #>
    Method.setup @{binding coherent}