src/Pure/Isar/element.ML

--- a/src/Pure/Isar/element.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/Isar/element.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -273,7 +273,7 @@
 
 fun prove_witness ctxt t tac =
   Witness (t,
-    Thm.close_derivation
+    Thm.close_derivation \<^here>
       (Goal.prove ctxt [] [] (mark_witness t)
         (fn _ => resolve_tac ctxt [Drule.protectI] 1 THEN tac)));
 
@@ -290,7 +290,7 @@
       (map o map) (fn prop => (mark_witness prop, [])) wit_propss @
         [map (rpair []) eq_props];
     fun after_qed' thmss =
-      let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
+      let val (wits, eqs) = split_last ((map o map) (Thm.close_derivation \<^here>) thmss);
       in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
   in proof after_qed' propss #> refine_witness end;
 
@@ -322,7 +322,7 @@
 end;
 
 fun conclude_witness ctxt (Witness (_, th)) =
-  Thm.close_derivation (Raw_Simplifier.norm_hhf_protect ctxt (Goal.conclude th));
+  Thm.close_derivation \<^here> (Raw_Simplifier.norm_hhf_protect ctxt (Goal.conclude th));
 
 fun pretty_witness ctxt witn =
   let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in