src/Pure/drule.ML

     #> Thm.varifyT_global);
 
 val export_without_context =
   flexflex_unique NONE
   #> export_without_context_open
-  #> Thm.close_derivation;
+  #> Thm.close_derivation \<^here>;
 
 
 (*Rotates a rule's premises to the left by k*)
 fun rotate_prems 0 = I
   | rotate_prems k = Thm.permute_prems 0 k;