src/Pure/Isar/element.ML

--- a/src/Pure/Isar/element.ML	Mon Aug 12 21:22:40 2019 +0200
+++ b/src/Pure/Isar/element.ML	Tue Aug 13 10:27:21 2019 +0200
@@ -281,7 +281,7 @@
 local
 
 val refine_witness =
-  Proof.refine_singleton (Method.Basic (fn ctxt => Method.CONTEXT_TACTIC o
+  Proof.refine_singleton (Method.Basic (fn ctxt => CONTEXT_TACTIC o
     K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (resolve_tac ctxt [Drule.protectI]))))))));
 
 fun gen_witness_proof proof after_qed wit_propss eq_props =