diff -r 67580f2ded90 -r 11d8517d9384 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Aug 12 21:22:40 2019 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Aug 13 10:27:21 2019 +0200
@@ -432,7 +432,7 @@
   refine_singleton (Method.Basic (K (Method.insert ths)));
 
 fun refine_primitive r =
-  refine_singleton (Method.Basic (fn ctxt => fn _ => Method.CONTEXT_TACTIC (PRIMITIVE (r ctxt))));
+  refine_singleton (Method.Basic (fn ctxt => fn _ => CONTEXT_TACTIC (PRIMITIVE (r ctxt))));
 
 end;
 
@@ -973,7 +973,7 @@
   in map (Logic.mk_term o Var) vars end;
 
 fun refine_terms n =
-  refine_singleton (Method.Basic (fn ctxt => Method.CONTEXT_TACTIC o
+  refine_singleton (Method.Basic (fn ctxt => CONTEXT_TACTIC o
     K (HEADGOAL (PRECISE_CONJUNCTS n
       (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI]))))))));