# HG changeset patch
# User wenzelm
# Date 1565363689 -7200
# Node ID 41108e3e9ca5498f892528d0a71534b08f4f0cc0
# Parent  a9053fa3090961809843c390171ea653ee45325c
formal position for PThm nodes;

diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/HOLCF/Tools/cont_proc.ML
--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -57,7 +57,7 @@
     let
       (* should use "close_derivation" for thms that are used multiple times *)
       (* it seems to allow for sharing in explicit proof objects *)
-      val x' = Thm.close_derivation (k x)
+      val x' = Thm.close_derivation \<^here> (k x)
       val Lx = x' RS cont_L
     in (map (fn y => SOME (k y RS Lx)) ys, x') end
 
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_axiomatization.ML
--- a/src/HOL/Tools/BNF/bnf_axiomatization.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_axiomatization.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -89,7 +89,7 @@
     fun mk_wit_thms set_maps =
       Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
         (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
-      |> Thm.close_derivation
+      |> Thm.close_derivation \<^here>
       |> Conjunction.elim_balanced (length wit_goals)
       |> map2 (Conjunction.elim_balanced o length) wit_goalss
       |> (map o map) (Thm.forall_elim_vars 0);
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -252,7 +252,7 @@
           mk_simplified_set_tac ctxt (collect_set_map_of_bnf outer);
         val set'_eq_set =
           Goal.prove (*no sorry*) names_lthy [] [] goal tac
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
         val set' = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of set'_eq_set)));
       in
         (set', set'_eq_set)
@@ -274,7 +274,7 @@
           val goal = mk_Trueprop_mem (bd_bd', ordIso);
         in
           (bd', SOME (Goal.prove_sorry lthy [] [] goal (bd_ordIso_natLeq_tac o #context)
-            |> Thm.close_derivation))
+            |> Thm.close_derivation \<^here>))
         end
       else
         (bd, NONE);
@@ -308,7 +308,7 @@
           Goal.prove_sorry lthy [] [] goal
             (fn {context = ctxt, prems = _} =>
               mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer))
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         (map2 (curry mk_Trueprop_eq) sets sets_alt);
 
     fun map_cong0_tac ctxt =
@@ -342,7 +342,7 @@
       in
         Goal.prove_sorry lthy [] [] goal
           (fn {context = ctxt, prems = _} => mk_comp_in_alt_tac ctxt set_alt_thms)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     fun le_rel_OO_tac ctxt = mk_le_rel_OO_tac ctxt (le_rel_OO_of_bnf outer) (rel_mono_of_bnf outer)
@@ -465,7 +465,7 @@
         val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
       in
         Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
-          kill_in_alt_tac ctxt) |> Thm.close_derivation
+          kill_in_alt_tac ctxt) |> Thm.close_derivation \<^here>
       end;
 
     fun le_rel_OO_tac ctxt =
@@ -579,7 +579,7 @@
         val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
       in
         Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => lift_in_alt_tac ctxt)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     fun le_rel_OO_tac ctxt = rtac ctxt (le_rel_OO_of_bnf bnf) 1;
@@ -667,7 +667,7 @@
       in
         Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
           mk_permute_in_alt_tac ctxt src dest)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     fun le_rel_OO_tac ctxt = rtac ctxt (le_rel_OO_of_bnf bnf) 1;
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -1449,7 +1449,7 @@
           in
             Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
               mk_collect_set_map_tac ctxt (#set_map0 axioms))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val collect_set_map = Lazy.lazy mk_collect_set_map;
@@ -1464,7 +1464,7 @@
           in
             Goal.prove_sorry lthy [] [] in_mono_goal (fn {context = ctxt, prems = _} =>
               mk_in_mono_tac ctxt live)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val in_mono = Lazy.lazy mk_in_mono;
@@ -1479,7 +1479,7 @@
           in
             Goal.prove_sorry lthy [] [] in_cong_goal
               (fn {context = ctxt, prems = _} => (TRY o hyp_subst_tac ctxt THEN' rtac ctxt refl) 1)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val in_cong = Lazy.lazy mk_in_cong;
@@ -1501,7 +1501,7 @@
             Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
               unfold_thms_tac ctxt @{thms simp_implies_def} THEN
               mk_map_cong_tac ctxt (#map_cong0 axioms))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val map_cong = Lazy.lazy (mk_map_cong Logic.mk_implies);
@@ -1516,7 +1516,7 @@
             Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
               mk_inj_map_tac ctxt live (Lazy.force map_id) (Lazy.force map_comp) (#map_cong0 axioms)
                 (Lazy.force map_cong))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val inj_map = Lazy.lazy mk_inj_map;
@@ -1560,7 +1560,7 @@
                 (Lazy.force map_comp) (Lazy.force map_id) (#map_cong0 axioms)
                 (map Lazy.force set_map) (#set_bd axioms) (#bd_card_order axioms)
                 bd_Card_order bd_Cinfinite bd_Cnotzero)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val in_bd = Lazy.lazy mk_in_bd;
@@ -1578,7 +1578,7 @@
               (fn {context = ctxt, prems = _} => mk_rel_Grp_tac ctxt rel_OO_Grps (#map_id0 axioms)
                 (#map_cong0 axioms) (Lazy.force map_id) (Lazy.force map_comp)
                 (map Lazy.force set_map))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val rel_Grp = Lazy.lazy mk_rel_Grp;
@@ -1596,7 +1596,7 @@
               (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl)))
               (fn {context = ctxt, prems = _} =>
                 mk_rel_mono_tac ctxt rel_OO_Grps (Lazy.force in_mono))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         fun mk_rel_cong0 () =
@@ -1607,7 +1607,7 @@
             Goal.prove_sorry lthy [] []
               (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (cong_prems, cong_concl)))
               (fn {context = ctxt, prems = _} => (TRY o hyp_subst_tac ctxt THEN' rtac ctxt refl) 1)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val rel_mono = Lazy.lazy mk_rel_mono;
@@ -1619,7 +1619,7 @@
               HOLogic.eq_const CA'))
             (fn {context = ctxt, prems = _} =>
               mk_rel_eq_tac ctxt live (Lazy.force rel_Grp) (Lazy.force rel_cong0) (#map_id0 axioms))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         val rel_eq = Lazy.lazy mk_rel_eq;
 
@@ -1633,13 +1633,13 @@
               (fn {context = ctxt, prems = _} => mk_rel_conversep_le_tac ctxt rel_OO_Grps
                 (Lazy.force rel_eq) (#map_cong0 axioms) (Lazy.force map_comp)
                 (map Lazy.force set_map))
-              |> Thm.close_derivation
+              |> Thm.close_derivation \<^here>
             val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
           in
             Goal.prove_sorry lthy [] [] goal
               (fn {context = ctxt, prems = _} =>
                 mk_rel_conversep_tac ctxt le_thm (Lazy.force rel_mono))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val rel_conversep = Lazy.lazy mk_rel_conversep;
@@ -1649,7 +1649,7 @@
             (fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (mk_leq rel_OO_lhs rel_OO_rhs)))
             (fn {context = ctxt, prems = _} => mk_rel_OO_le_tac ctxt rel_OO_Grps (Lazy.force rel_eq)
               (#map_cong0 axioms) (Lazy.force map_comp) (map Lazy.force set_map))
-          |> Thm.close_derivation
+          |> Thm.close_derivation \<^here>
           |> (fn thm => @{thm antisym} OF [thm, #le_rel_OO axioms]);
 
         val rel_OO = Lazy.lazy mk_rel_OO;
@@ -1679,7 +1679,7 @@
               (fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl)))
               (fn {context = ctxt, prems = _} => mk_rel_mono_strong0_tac ctxt (Lazy.force in_rel)
                 (map Lazy.force set_map))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val rel_mono_strong0 = Lazy.lazy mk_rel_mono_strong0;
@@ -1704,7 +1704,7 @@
             |> (fn vars => Goal.prove_sorry lthy vars (prem0 :: prem1 :: prems) eq
               (fn {context = ctxt, prems} =>
                 mk_rel_cong_tac ctxt (chop 2 prems) (Lazy.force rel_mono_strong)))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val rel_cong = Lazy.lazy (mk_rel_cong Logic.mk_implies);
@@ -1722,7 +1722,7 @@
             Goal.prove_sorry lthy [] []
               (fold_rev Logic.all (Ps @ Ps_copy) (Logic.list_implies (cong_prems, cong_concl)))
               (fn {context = ctxt, prems = _} => (TRY o hyp_subst_tac ctxt THEN' rtac ctxt refl) 1)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val pred_cong0 = Lazy.lazy mk_pred_cong0;
@@ -1735,7 +1735,7 @@
             Goal.prove_sorry lthy (map fst Ps') [] (mk_Trueprop_eq (lhs, rhs))
               (fn {context = ctxt, prems = _} =>
                 mk_rel_eq_onp_tac ctxt (#pred_set axioms) (#map_id0 axioms) (Lazy.force rel_Grp))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val rel_eq_onp = Lazy.lazy mk_rel_eq_onp;
@@ -1754,7 +1754,7 @@
               (fold_rev Logic.all (x :: Ps @ Ps_copy) (Logic.list_implies (prems, concl)))
               (fn {context = ctxt, prems = _} =>
                 mk_pred_mono_strong0_tac ctxt (Lazy.force pred_rel) (Lazy.force rel_mono_strong0))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val pred_mono_strong0 = Lazy.lazy mk_pred_mono_strong0;
@@ -1770,7 +1770,7 @@
               (fold_rev Logic.all (Ps @ Ps_copy) (Logic.list_implies (mono_prems, mono_concl)))
               (fn {context = ctxt, prems = _} =>
                 mk_pred_mono_tac ctxt (Lazy.force rel_eq_onp) (Lazy.force rel_mono))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val pred_mono = Lazy.lazy mk_pred_mono;
@@ -1790,7 +1790,7 @@
             |> (fn vars => Goal.prove_sorry lthy vars (prem0 :: prems) eq
               (fn {context = ctxt, prems} =>
                 mk_rel_cong_tac ctxt (chop 1 prems) (Lazy.force pred_mono_strong)))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val pred_cong = Lazy.lazy (mk_pred_cong Logic.mk_implies);
@@ -1812,7 +1812,7 @@
               HEADGOAL (EVERY' [REPEAT_DETERM o etac ctxt conjE,
                 etac ctxt (Lazy.force map_cong) THEN_ALL_NEW
                   (etac ctxt @{thm bspec} THEN' assume_tac ctxt)]))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val map_cong_pred = Lazy.lazy mk_map_cong_pred;
@@ -1839,7 +1839,7 @@
                   (Lazy.force rel_Grp) (Lazy.force map_id)))
             |> map (unfold_thms lthy @{thms vimage2p_def[of id, simplified id_apply]
                  vimage2p_def[of _ id, simplified id_apply]})
-            |> map Thm.close_derivation
+            |> map (Thm.close_derivation \<^here>)
           end;
 
         val rel_map = Lazy.lazy mk_rel_map;
@@ -1869,7 +1869,7 @@
                 unfold_thms_tac ctxt [prop_conv_thm] THEN
                 HEADGOAL (rtac ctxt (Lazy.force thm RS sym RS @{thm ord_eq_le_trans})
                   THEN' rtac ctxt (Lazy.force rel_mono) THEN_ALL_NEW assume_tac ctxt))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val rel_reflp = Lazy.lazy (mk_rel_preserves mk_reflp @{thm reflp_eq} rel_eq);
@@ -1888,7 +1888,7 @@
                   Lazy.force rel_cong0 RS fun_cong RS fun_cong RS trans OF
                     replicate live @{thm eq_onp_True},
                   Lazy.force rel_eq RS fun_cong RS fun_cong RS trans, @{thm eqTrueI[OF refl]}])))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val pred_True = Lazy.lazy mk_pred_True;
@@ -1907,7 +1907,7 @@
                 unfold_thms_tac ctxt
                   (@{thms Ball_image_comp ball_empty} @ map Lazy.force set_map) THEN
                 HEADGOAL (rtac ctxt refl))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val pred_map = Lazy.lazy mk_pred_map;
@@ -1926,7 +1926,7 @@
               (fn {context = ctxt, prems = _} => mk_map_transfer_tac ctxt (Lazy.force rel_mono)
                 (Lazy.force in_rel) (map Lazy.force set_map) (#map_cong0 axioms)
                 (Lazy.force map_comp))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val map_transfer = Lazy.lazy mk_map_transfer;
@@ -1943,7 +1943,7 @@
             Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
               mk_pred_transfer_tac ctxt live (Lazy.force in_rel) (Lazy.force pred_map)
                 (Lazy.force pred_cong))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val pred_transfer = Lazy.lazy mk_pred_transfer;
@@ -1964,7 +1964,7 @@
               (fn {context = ctxt, prems = _} =>
                 mk_rel_transfer_tac ctxt (Lazy.force in_rel) (Lazy.force rel_map)
                   (Lazy.force rel_mono_strong))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val rel_transfer = Lazy.lazy mk_rel_transfer;
@@ -1985,7 +1985,7 @@
                 Goal.prove_sorry lthy vars [] goal
                   (fn {context = ctxt, prems = _} =>
                      mk_set_transfer_tac ctxt (Lazy.force in_rel) (map Lazy.force set_map))
-                |> Thm.close_derivation
+                |> Thm.close_derivation \<^here>
                 |> Conjunction.elim_balanced (length goals)
               end
           end;
@@ -2011,7 +2011,7 @@
             Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
               mk_inj_map_strong_tac ctxt (Lazy.force rel_eq) (Lazy.force rel_map)
                 (Lazy.force rel_mono_strong))
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val inj_map_strong = Lazy.lazy mk_inj_map_strong;
@@ -2074,12 +2074,12 @@
     fun mk_wit_thms set_maps =
       Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
         (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
         |> Conjunction.elim_balanced (length wit_goals)
         |> map2 (Conjunction.elim_balanced o length) wit_goalss
         |> (map o map) (Thm.forall_elim_vars 0);
   in
-    map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
+    map2 (Thm.close_derivation \<^here> oo Goal.prove_sorry lthy [] [])
       goals (map (fn tac => fn {context = ctxt, prems = _} =>
         unfold_thms_tac ctxt one_step_defs THEN tac ctxt) tacs)
     |> (fn thms => after_qed mk_wit_thms (map single thms) lthy)
@@ -2094,7 +2094,7 @@
     fun mk_triv_wit_thms tac set_maps =
       Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
         (fn {context = ctxt, prems = _} => TRYALL Goal.conjunction_tac THEN tac ctxt set_maps)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
         |> Conjunction.elim_balanced (length wit_goals)
         |> map2 (Conjunction.elim_balanced o length) wit_goalss
         |> (map o map) (Thm.forall_elim_vars 0);
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -655,7 +655,7 @@
         Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
           mk_ctor_iff_dtor_tac ctxt (map (SOME o Thm.ctyp_of lthy) [ctor_absT, fpT])
             (Thm.cterm_of lthy ctor) (Thm.cterm_of lthy dtor) ctor_dtor dtor_ctor)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val ctr_rhss =
@@ -784,7 +784,7 @@
           mk_rel_case_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust injects
             rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs)
         |> singleton (Proof_Context.export names_lthy lthy)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     fun derive_case_transfer rel_case_thm =
@@ -797,7 +797,7 @@
         Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
           mk_case_transfer_tac ctxt rel_case_thm case_thms)
         |> singleton (Proof_Context.export names_lthy lthy)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
   in
     if live = 0 then
@@ -877,7 +877,7 @@
             Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
               mk_map_tac ctxt abs_inverses pre_map_def map_ctor_thm live_nesting_map_id0s ctr_defs'
                 extra_unfolds_map)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
             |> Conjunction.elim_balanced (length goals)
           end;
 
@@ -906,7 +906,7 @@
                 Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
                   mk_set0_tac ctxt abs_inverses pre_set_defs dtor_ctor fp_set_thms
                     fp_nesting_set_maps live_nesting_set_maps ctr_defs' extra_unfolds_set)
-                |> Thm.close_derivation
+                |> Thm.close_derivation \<^here>
                 |> Conjunction.elim_balanced (length goals)
               end
           end;
@@ -953,7 +953,7 @@
             Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
               mk_rel_tac ctxt abs_inverses pre_rel_def rel_ctor_thm live_nesting_rel_eqs ctr_defs'
                 extra_unfolds_rel)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
             |> Conjunction.elim_balanced (length goals)
           end;
 
@@ -979,7 +979,7 @@
                    Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
                      mk_rel_tac ctxt abs_inverses pre_rel_def rel_ctor_thm live_nesting_rel_eqs
                        ctr_defs' extra_unfolds_rel)
-                   |> Thm.close_derivation
+                   |> Thm.close_derivation \<^here>
                    |> Conjunction.elim_balanced (length goals)
                  end)
           end;
@@ -1012,7 +1012,7 @@
             Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} =>
                  mk_ctr_transfer_tac ctxt rel_intro_thms live_nesting_rel_eqs)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
             |> Conjunction.elim_balanced (length goals)
           end;
 
@@ -1066,7 +1066,7 @@
                 val thm =
                   Goal.prove_sorry lthy vars (flat premss) goal (fn {context = ctxt, prems} =>
                     mk_set_cases_tac ctxt (Thm.cterm_of ctxt ta) prems exhaust set_thms)
-                  |> Thm.close_derivation
+                  |> Thm.close_derivation \<^here>
                   |> rotate_prems ~1;
 
                 val cases_set_attr =
@@ -1117,7 +1117,7 @@
                  in
                    Goal.prove_sorry lthy vars [] goal
                      (fn {context = ctxt, prems = _} => mk_set_intros_tac ctxt set0_thms)
-                   |> Thm.close_derivation
+                   |> Thm.close_derivation \<^here>
                    |> Conjunction.elim_balanced (length goals)
                  end)
           end;
@@ -1150,7 +1150,7 @@
                 mk_rel_sel_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust
                   (flat disc_thmss) (flat sel_thmss) rel_inject_thms distincts rel_distinct_thms
                   live_nesting_rel_eqs))
-              |> Thm.close_derivation;
+              |> Thm.close_derivation \<^here>;
           in
             map prove goals
           end;
@@ -1183,7 +1183,7 @@
                   Goal.prove_sorry lthy vars [] goal
                     (fn {context = ctxt, prems = _} =>
                        mk_sel_transfer_tac ctxt n sel_defs case_transfer_thm)
-                  |> Thm.close_derivation
+                  |> Thm.close_derivation \<^here>
                   |> Conjunction.elim_balanced (length goals)
                 end
             end;
@@ -1201,7 +1201,7 @@
                   (fn {context = ctxt, prems = _} => mk_disc_transfer_tac ctxt
                      (the_single rel_sel_thms) (the_single exhaust_discs)
                      (flat (flat distinct_discsss)))
-                |> Thm.close_derivation
+                |> Thm.close_derivation \<^here>
                 |> Conjunction.elim_balanced (length goals)
               end
           end;
@@ -1230,7 +1230,7 @@
                   (fn {context = ctxt, prems = _} =>
                      mk_map_disc_iff_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss)
                        map_thms)
-                |> Thm.close_derivation
+                |> Thm.close_derivation \<^here>
                 |> Conjunction.elim_balanced (length goals)
               end
           end;
@@ -1270,7 +1270,7 @@
                      (fn {context = ctxt, prems = _} =>
                         mk_map_sel_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss)
                           map_thms (flat sel_thmss) live_nesting_map_id0s)
-                   |> Thm.close_derivation
+                   |> Thm.close_derivation \<^here>
                    |> Conjunction.elim_balanced (length goals)
                  end)
           end;
@@ -1334,7 +1334,7 @@
                      (fn {context = ctxt, prems = _} =>
                         mk_set_sel_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss)
                           (flat sel_thmss) set0_thms)
-                   |> Thm.close_derivation
+                   |> Thm.close_derivation \<^here>
                    |> Conjunction.elim_balanced (length goals)
                  end)
           end;
@@ -1744,7 +1744,7 @@
       Goal.prove_sorry ctxt vars prems goal (fn {context = ctxt, prems} =>
         mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (Thm.cterm_of ctxt) IRs) exhausts
           ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs)
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
   in
     (postproc_co_induct ctxt nn @{thm predicate2D} @{thm predicate2D_conj} rel_induct0_thm,
      mk_induct_attrs ctrAss)
@@ -1796,7 +1796,7 @@
           Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, ...} =>
             mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' pre_abs_inverses
               abs_inverses fp_nesting_set_maps pre_set_defss)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         `(conj_dests nn) thm
       end;
@@ -1838,7 +1838,7 @@
 
         fun prove goal tac =
           Goal.prove_sorry ctxt [] [] goal (tac o #context)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         map2 (map2 prove) goalss tacss
       end;
@@ -1947,7 +1947,7 @@
           (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars)
           (map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects
           rel_pre_defs abs_inverses live_nesting_rel_eqs)
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
   in
     (postproc_co_induct ctxt nn @{thm predicate2D} @{thm predicate2D_conj} rel_coinduct0_thm,
      mk_coinduct_attrs fpA_Ts (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss)
@@ -2028,7 +2028,7 @@
             (fn {context = ctxt, prems} =>
                mk_set_induct0_tac ctxt (map (Thm.cterm_of ctxt'') Ps) prems dtor_set_inducts
                  exhausts set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         val case_names_attr = Attrib.case_names (quasi_unambiguous_case_names case_names);
         val induct_set_attrs = map (Attrib.internal o K o Induct.induct_pred o name_of_set) sets;
@@ -2115,7 +2115,7 @@
       |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, ...} =>
         mk_coinduct_tac ctxt live_nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs pre_abs_inverses
           abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss))
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
 
     val rel_eqs = map rel_eq_of_bnf pre_bnfs;
     val rel_monos = map rel_mono_of_bnf pre_bnfs;
@@ -2202,7 +2202,7 @@
 
         fun prove goal tac =
           Goal.prove_sorry ctxt [] [] goal (tac o #context)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         map2 (map2 prove) goalss tacss
         |> map (map (unfold_thms ctxt @{thms case_sum_if}))
@@ -2226,7 +2226,7 @@
         fun prove goal tac =
           Variable.add_free_names ctxt goal []
           |> (fn vars => Goal.prove_sorry ctxt vars [] goal (tac o #context))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         fun proves [_] [_] = []
           | proves goals tacs = map2 prove goals tacs;
@@ -2565,7 +2565,7 @@
              mk_rec_transfer_tac ctxt nn ns (map (Thm.cterm_of ctxt) Ss)
                (map (Thm.cterm_of ctxt) Rs) xsssss rec_defs xtor_co_rec_transfers pre_rel_defs
                live_nesting_rel_eqs)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
         |> Conjunction.elim_balanced nn
       end;
 
@@ -2626,7 +2626,7 @@
                 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
                   mk_co_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s
                     abs_inverses ctor_rec_o_map)
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               rec_o_map_goals rec_defs xtor_co_rec_o_maps;
         in
           map single rec_o_map_thms
@@ -2717,7 +2717,7 @@
              mk_corec_transfer_tac ctxt (map (Thm.cterm_of ctxt) Ss) (map (Thm.cterm_of ctxt) Rs)
                type_definitions corec_defs xtor_co_rec_transfers pre_rel_defs
                live_nesting_rel_eqs (flat pgss) pss qssss gssss)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
         |> Conjunction.elim_balanced (length goals)
       end;
 
@@ -2773,7 +2773,7 @@
                 Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
                   mk_co_rec_o_map_tac ctxt corec_def pre_map_defs live_nesting_map_ident0s
                     abs_inverses dtor_map_o_corec)
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               map_o_corec_goals corec_defs xtor_co_rec_o_maps;
         in
           map single map_o_corec_thms
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -36,7 +36,7 @@
   in
     Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 val cacheN = "cache"
@@ -473,7 +473,7 @@
         |> HOLogic.mk_Trueprop
         |> (fn goal => Goal.prove_sorry raw_lthy [] [] goal
           (fn {context = ctxt, prems = _} => mk_xtor_un_fold_tac ctxt n simps cache_defs))
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
         |> Morphism.thm phi
         |> split_conj_thm
         |> map (fn thm => thm RS @{thm comp_eq_dest})
@@ -512,7 +512,7 @@
         Goal.prove_sorry raw_lthy vars prems concl
           (mk_xtor_un_fold_unique_tac fp un_fold_defs map_arg_congs xtor_un_fold_o_maps
             Rep_o_Abss fp_un_fold_uniques simp_thms map_thms map_defs cache_defs)
-          |> Thm.close_derivation
+          |> Thm.close_derivation \<^here>
           |> case_fp fp I (fn thm => thm OF replicate n sym)
           |> Morphism.thm phi
       end;
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -133,7 +133,7 @@
     in
       Goal.prove lthy vars [] goal (fn {context = ctxt, prems = _} =>
         mk_lfp_rec_sugar_transfer_tac ctxt def)
-      |> Thm.close_derivation
+      |> Thm.close_derivation \<^here>
     end);
 
 val gfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation
@@ -162,7 +162,7 @@
            (maps (#xtor_co_rec_transfers o #fp_res) fp_sugars)
            (map (rel_def_of_bnf o #pre_bnf) fp_sugars)
            disc_eq_cases case_thms case_distribs case_congs)
-       |> Thm.close_derivation
+       |> Thm.close_derivation \<^here>
      end);
 
 val _ = Theory.setup (lfp_rec_sugar_interpretation transfer_plugin
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -567,7 +567,7 @@
       (map2 (flip mk_leq) relphis pre_phis));
   in
     Goal.prove_sorry lthy (map (fst o dest_Free) (phis @ pre_phis)) prems concl tac
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
     |> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]}))
   end;
 
@@ -586,7 +586,7 @@
       (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers));
   in
     Goal.prove_sorry lthy [] [] goal tac
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
     |> split_conj_thm
   end;
 
@@ -796,7 +796,7 @@
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtor_thms
             xtor_un_fold_unique xtor_un_folds map_comps)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
         |> split_conj_thm
       end;
 
@@ -825,7 +825,7 @@
           |> (fn vars => Goal.prove_sorry lthy vars [] goal
             (fn {context = ctxt, prems = _} =>
               mk_xtor_co_rec_tac ctxt un_fold co_rec_defs co_rec_expand_thms))
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         goals xtor_un_folds
       end;
 
@@ -856,7 +856,7 @@
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs
             co_rec_expand'_thms xtor_un_fold_unique map_id0s sym_map_comp0s inverses)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val xtor_co_rec_o_map_thms = if forall is_none absT_info_opts
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -213,7 +213,7 @@
       in
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
@@ -231,7 +231,7 @@
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal))
           (fn {context = ctxt, prems = _} => mk_map_cong0L_tac ctxt m map_cong0 map_id)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
@@ -251,7 +251,7 @@
           Variable.add_free_names lthy goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
             (hyp_subst_tac ctxt THEN' rtac ctxt refl) 1))
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         goals
       end;
 
@@ -321,7 +321,7 @@
           Variable.add_free_names lthy goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
             mk_coalg_set_tac ctxt coalg_def))
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         goals) goalss
       end;
 
@@ -336,7 +336,7 @@
           (fn {context = ctxt, prems = _} => (rtac ctxt (coalg_def RS iffD2) 1 THEN CONJ_WRAP
             (K (EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
               CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm subset_UNIV}])) allAs] 1)) ss))
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val timer = time (timer "Coalgebra definition & thms");
@@ -416,7 +416,7 @@
           Variable.add_free_names lthy goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
             mk_mor_elim_tac ctxt mor_def))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         (map prove image_goals, map prove elim_goals)
       end;
@@ -431,7 +431,7 @@
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
           (fn {context = ctxt, prems = _} => mk_mor_incl_tac ctxt mor_def map_ids)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val mor_id_thm = mor_incl_thm OF (replicate n subset_refl);
@@ -448,7 +448,7 @@
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
           (fn {context = ctxt, prems = _} =>
             mk_mor_comp_tac ctxt mor_def mor_image'_thms morE_thms map_comp_id_thms)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val mor_cong_thm =
@@ -460,7 +460,7 @@
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
           (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val mor_UNIV_thm =
@@ -474,7 +474,7 @@
       in
         Goal.prove_sorry lthy vars [] (mk_Trueprop_eq (lhs, rhs))
           (fn {context = ctxt, prems = _} => mk_mor_UNIV_tac ctxt morE_thms mor_def)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val mor_str_thm =
@@ -486,7 +486,7 @@
       in
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_mor_str_tac ctxt ks mor_UNIV_thm)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val timer = time (timer "Morphism definition & thms");
@@ -567,7 +567,7 @@
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
           (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val bis_rel_thm =
@@ -586,7 +586,7 @@
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_bis_rel_tac ctxt m bis_def in_rels map_comps
             map_cong0s set_mapss)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val bis_converse_thm =
@@ -598,7 +598,7 @@
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_bis_converse_tac ctxt m bis_rel_thm rel_congs
             rel_converseps)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val bis_O_thm =
@@ -612,7 +612,7 @@
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
           (fn {context = ctxt, prems = _} => mk_bis_O_tac ctxt m bis_rel_thm rel_congs le_rel_OOs)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val bis_Gr_thm =
@@ -623,7 +623,7 @@
         Goal.prove_sorry lthy vars [] (Logic.list_implies ([coalg_prem, mor_prem], concl))
           (fn {context = ctxt, prems = _} => mk_bis_Gr_tac ctxt bis_rel_thm rel_Grps mor_image_thms
             morE_thms coalg_in_thms)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val bis_image2_thm = bis_cong_thm OF
@@ -644,7 +644,7 @@
       in
         Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, concl))
           (fn {context = ctxt, prems = _} => mk_bis_Union_tac ctxt bis_def in_mono'_thms)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     (* self-bisimulation *)
@@ -706,7 +706,7 @@
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} =>
             mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union_thm bis_cong_thm)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS
@@ -723,7 +723,7 @@
           Variable.add_free_names lthy goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
             mk_incl_lsbis_tac ctxt n i def))
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         goals ks lsbis_defs
       end;
 
@@ -737,7 +737,7 @@
           |> (fn vars => Goal.prove_sorry lthy vars [] goal
             (fn {context = ctxt, prems = _} => mk_equiv_lsbis_tac ctxt sbis_lsbis_thm l_incl incl_l
               bis_Id_on_thm bis_converse_thm bis_O_thm)
-          |> Thm.close_derivation))
+          |> Thm.close_derivation \<^here>))
         goals lsbis_incl_thms incl_lsbis_thms
       end;
 
@@ -968,7 +968,7 @@
       Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_coalg carTAs strTAs))
         (fn {context = ctxt, prems = _} => mk_coalgT_tac ctxt m
           (coalg_def :: isNode_defs @ carT_defs) strT_defs set_mapss)
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
 
     val timer = time (timer "Tree coalgebra");
 
@@ -1144,7 +1144,7 @@
         val length_Lev =
           Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
             (fn {context = ctxt, prems = _} => mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         val length_Lev' = mk_specN (n + 1) length_Lev;
         val length_Levs = map (fn i => length_Lev' RS mk_conjunctN n i RS mp) ks;
@@ -1159,7 +1159,7 @@
             Variable.add_free_names lthy goal []
             |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
               mk_length_Lev'_tac ctxt length_Lev))
-            |> Thm.close_derivation)
+            |> Thm.close_derivation \<^here>)
           goals length_Levs;
       in
         (length_Levs, length_Levs')
@@ -1183,7 +1183,7 @@
         val rv_last =
           Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
             (fn {context = ctxt, prems = _} => mk_rv_last_tac ctxt cTs cts rv_Nils rv_Conss)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         val rv_last' = mk_specN (n + 1) rv_last;
       in
@@ -1221,7 +1221,7 @@
           Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
             (fn {context = ctxt, prems = _} =>
               mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         val set_Lev' = mk_specN (3 * n + 1) set_Lev;
       in
@@ -1262,7 +1262,7 @@
             (fn {context = ctxt, prems = _} =>
               mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss
                 from_to_sbd_thmss to_sbd_inj_thmss)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         val set_image_Lev' = mk_specN (2 * n + 2) set_image_Lev;
       in
@@ -1283,7 +1283,7 @@
             to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss
             length_Lev_thms length_Lev'_thms rv_last_thmss set_Lev_thmsss
             set_image_Lev_thmsss set_mapss map_comp_id_thms map_cong0s)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val timer = time (timer "Behavioral morphism");
@@ -1312,7 +1312,7 @@
           Goal.prove_sorry lthy [] [] goal
             (fn {context = ctxt, prems = _} => mk_congruent_str_final_tac ctxt m lsbisE map_comp_id
               map_cong0 equiv_LSBIS_thms)
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         goals lsbisE_thms map_comp_id_thms map_cong0s
       end;
 
@@ -1320,13 +1320,13 @@
       (HOLogic.mk_Trueprop (mk_coalg car_finals str_finals))
       (fn {context = ctxt, prems = _} => mk_coalg_final_tac ctxt m coalg_def
         congruent_str_final_thms equiv_LSBIS_thms set_mapss coalgT_set_thmss)
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
 
     val mor_T_final_thm = Goal.prove_sorry lthy [] []
       (HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finals str_finals (map mk_proj lsbisAs)))
       (fn {context = ctxt, prems = _} => mk_mor_T_final_tac ctxt mor_def congruent_str_final_thms
         equiv_LSBIS_thms)
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
 
     val mor_final_thm = mor_comp_thm OF [mor_beh_thm, mor_T_final_thm];
     val in_car_final_thms = map (fn thm => thm OF [mor_final_thm, UNIV_I]) mor_image'_thms;
@@ -1404,14 +1404,14 @@
             (HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts))
             (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt (mor_def :: dtor_defs) Reps
               Abs_inverses coalg_final_set_thmss map_comp_id_thms map_cong0L_thms)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         val mor_Abs =
           Goal.prove_sorry lthy [] []
             (HOLogic.mk_Trueprop (mk_mor car_finals str_finals UNIVs dtors Abs_Ts))
             (fn {context = ctxt, prems = _} => mk_mor_Abs_tac ctxt (mor_def :: dtor_defs)
               Abs_inverses)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         (mor_Rep, mor_Abs)
       end;
@@ -1462,7 +1462,7 @@
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_mor_unfold_tac ctxt m mor_UNIV_thm dtor_defs
             unfold_defs Abs_inverses' morEs' map_comp_id_thms map_cong0s)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
     val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms;
 
@@ -1477,7 +1477,7 @@
           (fn {context = ctxt, prems = _} => mk_raw_coind_tac ctxt bis_def bis_cong_thm bis_O_thm
             bis_converse_thm bis_Gr_thm tcoalg_thm coalgT_thm mor_T_final_thm sbis_lsbis_thm
             lsbis_incl_thms incl_lsbis_thms equiv_LSBIS_thms mor_Rep_thm Rep_injects)
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
       end;
 
     val (unfold_unique_mor_thms, unfold_unique_mor_thm) =
@@ -1494,7 +1494,7 @@
         val unique_mor = Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique))
           (fn {context = ctxt, prems = _} => mk_unfold_unique_mor_tac ctxt raw_coind_thms
             bis_thm mor_thm unfold_defs)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         `split_conj_thm unique_mor
       end;
@@ -1550,7 +1550,7 @@
           Goal.prove_sorry lthy [] [] goal
             (fn {context = ctxt, prems = _} => mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id
               map_cong0L unfold_o_dtor_thms)
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
           goals ctor_defs dtor_unfold_thms map_comp_id_thms map_cong0L_thms
       end;
 
@@ -1608,7 +1608,7 @@
           |> (fn vars => Goal.prove_sorry lthy vars [] dtor_coinduct_goal
             (fn {context = ctxt, prems = _} => mk_dtor_coinduct_tac ctxt m raw_coind_thm bis_rel_thm
               rel_congs))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         (rev (Term.add_tfrees dtor_coinduct_goal []), dtor_coinduct)
       end;
@@ -1834,7 +1834,7 @@
                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
                      mk_map_tac ctxt m n map_arg_cong unfold map_comp map_cong0))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               goals dtor_unfold_thms map_comps map_cong0s map_arg_cong_thms;
           in
             map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps
@@ -1854,7 +1854,7 @@
             `split_conj_thm (Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal))
               (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
                 mk_dtor_map_unique_tac ctxt dtor_unfold_unique_thm sym_map_comps)
-            |> Thm.close_derivation)
+            |> Thm.close_derivation \<^here>)
           end;
 
         val Jmap_comp0_thms =
@@ -1868,7 +1868,7 @@
             split_conj_thm (Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} =>
                 mk_map_comp0_tac ctxt Jmap_thms map_comp0s dtor_Jmap_unique_thm)
-              |> Thm.close_derivation)
+              |> Thm.close_derivation \<^here>)
           end;
 
         val timer = time (timer "map functions for the new codatatypes");
@@ -1907,7 +1907,7 @@
                   |> (fn vars => Goal.prove_sorry lthy vars [] goal
                     (fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s
                       col_Sucs))
-                  |> Thm.close_derivation)
+                  |> Thm.close_derivation \<^here>)
                 goals ctss col_0ss' col_Sucss'
               end;
 
@@ -1923,7 +1923,7 @@
                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
                 (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
                   mk_Jset_minimal_tac ctxt n col_minimal))
-              |> Thm.close_derivation)
+              |> Thm.close_derivation \<^here>)
             goals col_minimal_thms
           end;
 
@@ -1955,7 +1955,7 @@
                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
                     mk_set_incl_Jset_tac ctxt rec_Suc))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               goals rec_Sucs)
             set_incl_Jset_goalss col_Sucss,
             map2 (fn goalss => fn rec_Sucs =>
@@ -1965,7 +1965,7 @@
                   |> (fn vars => Goal.prove_sorry lthy vars [] goal
                     (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
                       mk_set_Jset_incl_Jset_tac ctxt n rec_Suc k))
-                  |> Thm.close_derivation)
+                  |> Thm.close_derivation \<^here>)
                 goals rec_Sucs)
               ks goalss)
             set_Jset_incl_Jset_goalsss col_Sucss)
@@ -2024,7 +2024,7 @@
                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
                   (fn {context = ctxt, prems = _} =>
                     mk_set_le_tac ctxt n Jset_minimal set_Jsets set_Jset_Jsetss))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               le_goals Jset_minimal_thms set_Jset_thmss' set_Jset_Jset_thmsss');
 
             val ge_goalss = map (map HOLogic.mk_Trueprop) (mk_goals (uncurry mk_leq o swap));
@@ -2034,7 +2034,7 @@
                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
                   (fn {context = ctxt, prems = _} =>
                     mk_set_ge_tac ctxt n set_incl_Jset set_Jset_incl_Jsets))
-                |> Thm.close_derivation))
+                |> Thm.close_derivation \<^here>))
               ge_goalss set_incl_Jset_thmss' set_Jset_incl_Jset_thmsss'
           in
             map2 (map2 (fn le => fn ge => equalityI OF [le, ge])) set_le_thmss set_ge_thmss
@@ -2067,7 +2067,7 @@
                 |> (fn vars => Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
                   (fn {context = ctxt, prems = _} => mk_col_natural_tac ctxt cts rec_0s rec_Sucs
                     dtor_Jmap_thms set_mapss))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               goals ctss col_0ss' col_Sucss';
           in
             map (split_conj_thm o mk_specN n) thms
@@ -2091,7 +2091,7 @@
                 |> (fn vars => Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN
                     mk_col_bd_tac ctxt m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               ls goals ctss col_0ss' col_Sucss';
           in
             map (split_conj_thm o mk_specN n) thms
@@ -2138,7 +2138,7 @@
                 (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt m (rtac ctxt coinduct) map_comps
                   dtor_Jmap_thms map_cong0s
                   set_mapss set_Jset_thmss set_Jset_Jset_thmsss in_rels)
-              |> Thm.close_derivation;
+              |> Thm.close_derivation \<^here>;
           in
             split_conj_thm thm
           end;
@@ -2169,7 +2169,7 @@
                 (fn {context = ctxt, prems = _} =>
                   mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets
                     dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss))
-              |> Thm.close_derivation)
+              |> Thm.close_derivation \<^here>)
             ks goals in_rels map_comps map_cong0s dtor_Jmap_thms dtor_Jset_thmss'
               dtor_inject_thms dtor_ctor_thms set_mapss dtor_Jset_incl_thmss
               dtor_set_Jset_incl_thmsss
@@ -2252,7 +2252,7 @@
                   mk_rel_coinduct_coind_tac ctxt fst m
                     (infer_instantiate' ctxt cts dtor_coinduct_thm) ks map_comps map_cong0s
                     map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms in_rels)
-              |> Thm.close_derivation
+              |> Thm.close_derivation \<^here>
               |> split_conj_thm
             end;
 
@@ -2291,7 +2291,7 @@
                 (fn {context = ctxt, prems = _} =>
                   mk_rel_coinduct_ind_tac ctxt m ks
                     dtor_unfold_thms set_mapss j (infer_instantiate' ctxt cts set_induct)))
-              |> Thm.close_derivation
+              |> Thm.close_derivation \<^here>
               |> split_conj_thm)
             mk_helper_ind_concls ls dtor_Jset_induct_thms ctss
             |> transpose;
@@ -2315,7 +2315,7 @@
           in
             Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
               mk_le_rel_OO_tac ctxt Jrel_coinduct_thm dtor_Jrel_thms le_rel_OOs)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val timer = time (timer "helpers for BNF properties");
@@ -2435,7 +2435,7 @@
               |> (fn vars => Goal.prove_sorry lthy vars [] goal
                 (fn {context = ctxt, prems = _} => mk_coind_wit_tac ctxt induct dtor_unfold_thms
                   (flat set_mapss) wit_thms))
-              |> Thm.close_derivation)
+              |> Thm.close_derivation \<^here>)
             goals dtor_Jset_induct_thms
             |> map split_conj_thm
             |> transpose
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_gfp_grec.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -881,7 +881,7 @@
     Variable.add_free_names ctxt goal []
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_sig_transfer_tac ctxt pre_rel_def preT_rel_eqs transfer_thm))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_transfer_by_transfer_prover ctxt live_AsBs Rs R const const_defs rel_eqs transfers =
@@ -893,7 +893,7 @@
     |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_transfer_by_transfer_prover_tac ctxt (const_defs @ map (fn thm => thm RS sym) rel_eqs)
         rel_eqs transfers))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_dtor_transfer ctxt live_EsFs Y Z pre_rel fp_rel Rs dtor dtor_rel_thm =
@@ -911,7 +911,7 @@
     Variable.add_free_names ctxt goal []
     |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_dtor_transfer_tac ctxt dtor_rel_thm))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_Lam_or_eval_core_transfer ctxt live_AsBs Y Z preT ssig_T Rs R pre_rel sig_or_ssig_rel
@@ -936,7 +936,7 @@
     Variable.add_free_names ctxt goal []
     |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_transfer_by_transfer_prover_tac ctxt [const_def] rel_eqs transfers))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_proto_sctr_transfer_step_or_merge ctxt Y Z R dead_pre_rel dead_sig_rel proto_sctr
@@ -949,7 +949,7 @@
     Variable.add_free_names ctxt goal []
     |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_transfer_by_transfer_prover_tac ctxt [proto_sctr_def] fp_k_T_rel_eqs transfers))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_sctr_transfer ctxt live_AsBs Y Z ssig_T Rs R pre_rel ssig_rel sctr sctr_def
@@ -967,7 +967,7 @@
     Variable.add_free_names ctxt goal []
     |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_transfer_by_transfer_prover_tac ctxt [sctr_def] fp_k_T_rel_eqs transfers))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_corecUU_transfer ctxt live_AsBs Y Z Rs R preT ssig_T pre_rel fp_rel ssig_rel corecUU
@@ -993,7 +993,7 @@
     |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_transfer_by_transfer_prover_tac ctxt [cutSsig_def, corecU_def, corecUU_def] fp_k_T_rel_eqs
         transfers))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun mk_natural_goal ctxt simple_T_mapfs fs t u =
@@ -1021,7 +1021,7 @@
     Variable.add_free_names ctxt goal []
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_natural_by_unfolding_tac ctxt map_thms))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_natural_from_transfer ctxt live_AsBs simple_T_mapfs fs f const transfer bnfs subst_bnfs =
@@ -1035,7 +1035,7 @@
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_natural_from_transfer_tac ctxt m (replicate m true) transfer [] (map rel_Grp_of_bnf bnfs)
         (map rel_Grp_of_bnf subst_bnfs)))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_natural_from_transfer_with_pre_type ctxt live_AsBs Y Z preT ssig_T pre_map ssig_map fs
@@ -1077,7 +1077,7 @@
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal
       (fn {context = ctxt, prems = _} => mk_Lam_Inl_Inr_tac ctxt unsig_thm Lam_def))
     |> Conjunction.elim_balanced (length goals)
-    |> map Thm.close_derivation
+    |> map (Thm.close_derivation \<^here>)
   end;
 
 fun derive_flat_VLeaf ctxt Y Z ssig_T x VLeaf dead_ssig_map flat ssig_induct fp_map_id sig_map_cong
@@ -1095,7 +1095,7 @@
       mk_flat_VLeaf_or_flat_tac ctxt ssig_induct' sig_map_cong
         (fp_map_id :: sig_map_ident :: sig_map_comp :: ssig_map_thms @ flat_simps @
          @{thms o_apply id_apply id_def[symmetric]})))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_flat_flat ctxt Y Z ssig_T x dead_ssig_map flat ssig_induct fp_map_id sig_map_cong
@@ -1116,7 +1116,7 @@
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_flat_VLeaf_or_flat_tac ctxt ssig_induct' sig_map_cong
         (o_apply :: fp_map_id :: sig_map_comp :: ssig_map_thms @ flat_simps)))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_eval_core_flat ctxt Y Z preT ssig_T dead_pre_map dead_ssig_map flat eval_core x
@@ -1148,7 +1148,7 @@
       mk_eval_core_flat_tac ctxt ssig_induct' dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp
         fp_map_id sig_map_comp sig_map_cong ssig_map_thms ssig_map_comp flat_simps
         flat_pointful_natural flat_flat Lam_pointful_natural eval_core_simps))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_eval_thm ctxt dtor_inject dtor_unfold_thm eval_def =
@@ -1177,7 +1177,7 @@
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_eval_flat_tac ctxt dead_pre_map_comp0 ssig_map_id ssig_map_comp flat_pointful_natural
         eval_core_pointful_natural eval_core_flat eval_thm cond_eval_o_flat))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_eval_Oper ctxt live Y Z fpT sig_T ssig_T dead_sig_map Oper eval algLam x sig_map_ident
@@ -1196,7 +1196,7 @@
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_eval_Oper_tac ctxt live sig_map_ident sig_map_comp0 sig_map_comp Oper_natural_pointful
         VLeaf_natural flat_simps eval_flat algLam_def))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_eval_V_or_CLeaf ctxt Y fpT V_or_CLeaf eval x dead_pre_map_id dead_pre_map_comp fp_map_id
@@ -1211,7 +1211,7 @@
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_eval_V_or_CLeaf_tac ctxt dead_pre_map_id dead_pre_map_comp fp_map_id dtor_unfold_unique
         V_or_CLeaf_map_thm eval_core_simps eval_thm))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_extdd_mor ctxt Y Z preT fpT ssig_T dead_pre_map dtor extdd cutSsig f g dead_pre_map_comp0
@@ -1235,7 +1235,7 @@
       mk_extdd_mor_tac ctxt dead_pre_map_comp0 dead_pre_map_comp VLeaf_map_thm ssig_map_comp
         flat_pointful_natural eval_core_pointful_natural eval_thm eval_flat eval_VLeaf cutSsig_def
         prem))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_mor_cutSsig_flat ctxt Y Z preT fpT ssig_T dead_pre_map dead_ssig_map dtor flat eval_core
@@ -1271,7 +1271,7 @@
         dead_pre_map_cong dtor_unfold_unique dead_ssig_map_comp0 ssig_map_comp flat_simps
         flat_pointful_natural eval_core_pointful_natural flat_flat flat_VLeaf eval_core_flat
         cutSsig_def cutSsig_def_pointful_natural eval_thm prem))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_extdd_o_VLeaf ctxt Y Z preT fpT ssig_T dead_pre_map dtor VLeaf extdd f g
@@ -1295,7 +1295,7 @@
     |> (fn vars => Goal.prove_sorry ctxt vars [prem] goal (fn {context = ctxt, prems = [prem]} =>
       mk_extdd_o_VLeaf_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_inject ssig_map_thms
         eval_core_simps eval_thm eval_VLeaf prem))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_corecU_pointfree ctxt Y Z preT fpT ssig_T dead_pre_map dtor extdd corecU g
@@ -1318,7 +1318,7 @@
       mk_corecU_pointfree_tac ctxt dead_pre_map_comp dtor_unfold_thm ssig_map_thms
       dead_ssig_map_comp0 flat_simps flat_VLeaf eval_core_simps cutSsig_def mor_cutSsig_flat
       corecU_def))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_corecU_ctor_unique ctxt Y Z preT fpT ssig_T dead_pre_map ctor dtor VLeaf extdd corecU f g
@@ -1386,7 +1386,7 @@
       mk_dtor_algLam_tac ctxt pre_map_comp dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp
         sig_map_comp Oper_pointful_natural ssig_map_thms dead_ssig_map_comp0 Lam_pointful_natural
         eval_core_simps eval_thm eval_flat eval_VLeaf algLam_def))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_algLam_base ctxt Y Z preT fpT dead_pre_map ctor dtor algLam proto_sctr dead_pre_map_id
@@ -1407,7 +1407,7 @@
       mk_algLam_base_tac ctxt dead_pre_map_dtor dead_pre_map_id dead_pre_map_comp ctor_dtor
         dtor_ctor dtor_unfold_unique unsig_thm Sig_pointful_natural ssig_map_thms Lam_def flat_simps
         eval_core_simps eval_thm algLam_def))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_flat_embL ctxt Y Z old_ssig_T ssig_T dead_old_ssig_map embL old_flat flat x
@@ -1431,7 +1431,7 @@
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_flat_embL_tac ctxt old_ssig_induct' fp_map_id Sig_pointful_natural old_sig_map_comp
         old_sig_map_cong old_ssig_map_thms old_flat_simps flat_simps embL_simps))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_eval_core_embL ctxt Y Z preT old_ssig_T ssig_T dead_pre_map embL old_eval_core eval_core
@@ -1457,7 +1457,7 @@
       mk_eval_core_embL_tac ctxt old_ssig_induct' dead_pre_map_comp0 dead_pre_map_comp
         Sig_pointful_natural unsig_thm old_sig_map_comp old_sig_map_cong old_Lam_pointful_natural
         Lam_def flat_embL old_eval_core_simps eval_core_simps embL_simps embL_pointful_natural))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_eval_embL ctxt Y fpT embL old_eval eval dead_pre_map_comp0 dtor_unfold_unique
@@ -1470,7 +1470,7 @@
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_eval_embL_tac ctxt dead_pre_map_comp0 dtor_unfold_unique embL_pointful_natural
         eval_core_embL old_eval_thm eval_thm))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_algLam_algLam ctxt Inx_const Y fpT Sig old_algLam algLam dead_pre_map_comp dtor_inject
@@ -1486,7 +1486,7 @@
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_algLam_algLam_tac ctxt dead_pre_map_comp dtor_inject unsig_thm sig_map_thm Lam_def
         eval_embL old_dtor_algLam dtor_algLam))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_eval_core_k_as_ssig ctxt Y preT k_T rho eval_core k_as_ssig x pre_map_comp
@@ -1505,7 +1505,7 @@
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_eval_core_k_as_ssig_tac ctxt pre_map_comp dead_pre_map_id sig_map_comp ssig_map_thms
         Lam_natural_pointful Lam_Inr flat_VLeaf eval_core_simps))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_algLam_algrho ctxt Y fpT Sig algLam algrho algLam_def algrho_def =
@@ -1519,7 +1519,7 @@
     Variable.add_free_names ctxt goal []
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_algLam_algrho_tac ctxt algLam_def algrho_def))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_dtor_algrho ctxt Y Z preT fpT k_T ssig_T dead_pre_map dead_k_map dtor rho eval algrho x
@@ -1543,7 +1543,7 @@
     Variable.add_free_names ctxt goal []
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_dtor_algrho_tac ctxt eval_thm k_as_ssig_natural_pointful eval_core_k_as_ssig algrho_def))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_algLam_step_or_merge ctxt Y fpT ctor proto_sctr algLam proto_sctr_def old_algLam_pointful
@@ -1557,7 +1557,7 @@
     Variable.add_free_names ctxt goal []
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_algLam_step_tac ctxt proto_sctr_def old_algLam_pointful algLam_algLam_pointful))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_eval_sctr ctxt Y Z fpT ssig_T dead_pre_map ctor eval sctr proto_sctr_pointful_natural
@@ -1574,7 +1574,7 @@
     Variable.add_free_names ctxt goal []
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_eval_sctr_tac ctxt proto_sctr_pointful_natural eval_Oper algLam_thm sctr_def))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_corecUU_pointfree_unique ctxt Y Z preT fpT ssig_T dead_pre_map ctor dead_ssig_map eval
@@ -1609,7 +1609,7 @@
           mk_corecUU_pointfree_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor dtor_inject
             ssig_map_comp flat_pointful_natural eval_core_pointful_natural eval_thm eval_flat
             corecU_ctor sctr_pointful_natural eval_sctr_pointful corecUU_def))
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val corecUU_unique =
@@ -1623,7 +1623,7 @@
                 mk_corecUU_unique_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor
                   ssig_map_comp flat_pointful_natural eval_core_pointful_natural eval_thm eval_flat
                   corecU_unique sctr_pointful_natural eval_sctr_pointful corecUU_def prem))
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
   in
     (corecUU_pointfree, corecUU_unique)
@@ -1858,7 +1858,7 @@
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_equivp_Retr_tac ctxt dead_pre_rel_refl_thm dead_pre_rel_flip_thm dead_pre_rel_mono_thm
         dead_pre_rel_compp_thm))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_Retr_coinduct ctxt fpT Retr R dtor_rel_coinduct_thm rel_eq_thm =
@@ -1868,7 +1868,7 @@
   in
     Goal.prove_sorry ctxt [] [] goal (fn {context = ctxt, prems = _} =>
       mk_Retr_coinduct_tac ctxt dtor_rel_coinduct_thm rel_eq_thm)
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_Retr fp_sugar fpT dead_pre_bnf ctor dtor names_lthy lthy =
@@ -1904,7 +1904,7 @@
   in
     Variable.add_free_names ctxt goal []
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} => tac ctxt))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_cong_general fp_b version fpT dead_ssig_bnf dead_pre_bnf eval Retr equivp_Retr
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -247,7 +247,7 @@
   in
     Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_case_dtor_tac ctxt u abs_inverse dtor_ctor ctr_defs exhaust case_thms)
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_case_trivial ctxt fpT_name =
@@ -269,7 +269,7 @@
     Goal.prove_sorry ctxt [var_name] [] goal (fn {context = ctxt, prems = _} =>
       HEADGOAL (rtac ctxt exhaust') THEN ALLGOALS (hyp_subst_tac ctxt) THEN
       unfold_thms_tac ctxt case_thms THEN ALLGOALS (rtac ctxt refl))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun mk_abs_rep_transfers ctxt fpT_name =
@@ -351,7 +351,7 @@
         live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs corecUU_thm
         all_sig_map_thms ssig_map_thms all_algLam_alg_pointfuls (all_algrho_eqs_of ctxt) eval_simps
         inner_fp_simps fun_def))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_unique ctxt phi code_goal
@@ -410,7 +410,7 @@
         live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs all_sig_map_thms
         ssig_map_thms all_algLam_alg_pointfuls (all_algrho_eqs_of ctxt) eval_simps corecUU_unique
         eq_corecUU)
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_last_disc ctxt fcT_name =
@@ -428,7 +428,7 @@
   in
     Goal.prove_sorry ctxt [fst (dest_Free u)] [] goal (fn {context = ctxt, prems = _} =>
       mk_last_disc_tac ctxt u exhaust (flat disc_thmss))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_eq_algrho ctxt {sig_fp_sugars, ssig_fp_sugar, eval, eval_simps, all_algLam_algs,
@@ -522,7 +522,7 @@
           disc_sel_eq_cases case_dtor case_eq_ifs const_pointful_naturals
           fp_nesting_k_map_disc_sels' rho_def dtor_algrho corecUU_unique eq_corecUU all_sig_map_thms
           ssig_map_thms all_algLam_alg_pointfuls (all_algrho_eqs_of ctxt) eval_simps)
-      |> Thm.close_derivation
+      |> Thm.close_derivation \<^here>
       handle e as ERROR _ =>
         (case filter (is_none o snd) (const_transfers ~~ const_pointful_natural_opts) of
           [] => Exn.reraise e
@@ -549,7 +549,7 @@
       Variable.add_free_names ctxt goal []
       |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
         unfold_thms_tac ctxt simps THEN HEADGOAL (rtac ctxt rho_transfer')))
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
 
     val goal' = Raw_Simplifier.rewrite_term thy simps [] goal;
   in
@@ -567,7 +567,7 @@
       mk_rho_transfer_tac ctxt (null abs_rep_transfers) (rel_def_of_bnf pre_bnf)
       const_transfers))
     |> unfold_thms ctxt [rho_def RS @{thm symmetric}]
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong alg =
@@ -606,7 +606,7 @@
       Variable.add_free_names ctxt goal []
       |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
         mk_cong_intro_ctr_or_friend_tac ctxt ctr_def [pre_rel_def, abs_inverse] cong_ctor_intro))
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
 
     val goals = map (mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong) ctrs;
   in
@@ -635,7 +635,7 @@
     Variable.add_free_names ctxt goal []
     |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_cong_intro_ctr_or_friend_tac ctxt eq_algrho [] cong_algrho_intro))
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_cong_intros lthy ctr_names friend_names
@@ -1912,7 +1912,7 @@
         live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs all_sig_map_thms
         ssig_map_thms all_algLam_alg_pointfuls (all_algrho_eqs_of ctxt) eval_simps corecUU_unique
         fun_code)
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 fun derive_coinduct_cong_intros
@@ -2167,7 +2167,7 @@
       Variable.add_free_names ctxt goal []
       |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
         HEADGOAL (Transfer.transfer_prover_tac ctxt)))
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
 
     fun maybe_prove_transfer_goal ctxt goal =
       (case try (prove_transfer_goal ctxt) goal of
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -101,7 +101,7 @@
         rtac ctxt refl);
   in
     Goal.prove_sorry ctxt [] [] goal (fn {context = ctxt, ...} => mk_tac ctxt)
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 val num_curry_uncurryN_balanced_precomp = 8;
@@ -239,7 +239,7 @@
     Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       mk_natural_from_transfer_tac ctxt m (replicate n true) transfer A_nesting_map_ids
         A_nesting_rel_Grps [])
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
   end;
 
 type s_parse_info =
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -1147,7 +1147,7 @@
         tac_opt;
 
     val excludess'' = @{map 3} (fn tac_opt => fn sequential => map (fn (j, goal) =>
-          (j, (Option.map (Goal.prove (*no sorry*) lthy [] [] goal #> Thm.close_derivation)
+          (j, (Option.map (Goal.prove (*no sorry*) lthy [] [] goal #> Thm.close_derivation \<^here>)
              (exclude_tac tac_opt sequential j), goal))))
         tac_opts sequentials excludess'
       handle ERROR _ => use_primcorecursive ();
@@ -1183,12 +1183,12 @@
               in
                 [Goal.prove (*no sorry*) lthy [] [] goal (fn {context = ctxt, ...} =>
                    mk_primcorec_nchotomy_tac ctxt (res_exhaust_discs @ arg_exhaust_discs))
-                 |> Thm.close_derivation]
+                 |> Thm.close_derivation \<^here>]
                 handle ERROR _ => use_primcorecursive ()
               end
             | false =>
               (case tac_opt of
-                SOME tac => [Goal.prove_sorry lthy [] [] goal tac |> Thm.close_derivation]
+                SOME tac => [Goal.prove_sorry lthy [] [] goal tac |> Thm.close_derivation \<^here>]
               | NONE => []))
         tac_opts corec_specs disc_eqnss nchotomy_goalss syntactic_exhaustives;
 
@@ -1232,7 +1232,7 @@
                     mk_primcorec_exhaust_tac ctxt
                       ("" (* for "P" *) :: map (fst o dest_Free) fun_args)
                       (length disc_eqns) nchotomy_thm)
-                 |> Thm.close_derivation])
+                 |> Thm.close_derivation \<^here>])
             disc_eqnss nchotomy_thmss;
         val nontriv_exhaust_thmss = map (filter_out is_trivial_implies) exhaust_thmss;
 
@@ -1266,7 +1266,7 @@
                 Goal.prove_sorry lthy [] [] goal
                   (fn {context = ctxt, prems = _} =>
                     mk_primcorec_disc_tac ctxt def_thms corec_disc k m excludesss)
-                |> Thm.close_derivation
+                |> Thm.close_derivation \<^here>
                 |> pair (#disc (nth ctr_specs ctr_no))
                 |> pair eqn_pos
                 |> single
@@ -1299,7 +1299,7 @@
                 mk_primcorec_sel_tac ctxt def_thms distincts split_sels split_sel_asms
                   fp_nesting_maps fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m
                   excludesss)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
             |> `(is_some code_rhs_opt ? Local_Defs.fold lthy sel_defs) (*mildly too aggressive*)
             |> pair sel
             |> pair eqn_pos
@@ -1349,7 +1349,7 @@
                   (fn {context = ctxt, prems = _} =>
                     mk_primcorec_ctr_tac ctxt m collapse disc_thm_opt sel_thms)
                 |> is_some code_rhs_opt ? Local_Defs.fold lthy sel_defs (*mildly too aggressive*)
-                |> Thm.close_derivation
+                |> Thm.close_derivation \<^here>
                 |> pair ctr
                 |> pair eqn_pos
                 |> single
@@ -1438,12 +1438,12 @@
                           mk_primcorec_raw_code_tac ctxt distincts discIs split_sels split_sel_asms
                             ms ctr_thms
                             (if exhaustive_code then try the_single nchotomys else NONE))
-                      |> Thm.close_derivation;
+                      |> Thm.close_derivation \<^here>;
                   in
                     Goal.prove_sorry lthy [] [] goal
                       (fn {context = ctxt, prems = _} =>
                         mk_primcorec_code_tac ctxt distincts split_sels raw_code_thm)
-                    |> Thm.close_derivation
+                    |> Thm.close_derivation \<^here>
                     |> single
                   end)
               end)
@@ -1473,7 +1473,7 @@
                 (fn {context = ctxt, prems = _} =>
                   mk_primcorec_disc_iff_tac ctxt (map (fst o dest_Free) exhaust_fun_args)
                     (the_single exhaust_thms) disc_thms disc_thmss' (flat distinct_discss))
-              |> Thm.close_derivation
+              |> Thm.close_derivation \<^here>
               |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve lthy thm rule)))
                 @{thms eqTrueE eq_False[THEN iffD1] notnotD}
               |> pair eqn_pos
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -191,7 +191,7 @@
       in
         Goal.prove_sorry lthy vars [] (mk_Trueprop_eq (lhs, rhs))
           (fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
@@ -208,7 +208,7 @@
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal))
           (fn {context = ctxt, prems = _} => mk_map_cong0L_tac ctxt m map_cong0 map_id)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
@@ -277,7 +277,7 @@
           Variable.add_free_names lthy goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
             mk_alg_set_tac ctxt alg_def))
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         goals
       end;
 
@@ -296,7 +296,7 @@
           |> (fn vars => Goal.prove_sorry lthy vars [] goal
             (fn {context = ctxt, prems = _} =>
               mk_alg_not_empty_tac ctxt alg_set alg_set_thms wit_thms))
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         goals alg_set_thms
       end;
 
@@ -372,7 +372,7 @@
           Variable.add_free_names lthy goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
             mk_mor_elim_tac ctxt mor_def))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         map prove elim_goals
       end;
@@ -385,7 +385,7 @@
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
           (fn {context = ctxt, prems = _} => mk_mor_incl_tac ctxt mor_def map_ids)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val mor_comp_thm =
@@ -399,7 +399,7 @@
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
           (fn {context = ctxt, prems = _} => mk_mor_comp_tac ctxt mor_def set_mapss map_comp_id_thms)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val mor_cong_thm =
@@ -411,7 +411,7 @@
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
           (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val mor_str_thm =
@@ -424,7 +424,7 @@
       in
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_mor_str_tac ctxt ks mor_def)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val mor_UNIV_thm =
@@ -438,7 +438,7 @@
       in
         Goal.prove_sorry lthy vars [] (mk_Trueprop_eq (lhs, rhs))
           (fn {context = ctxt, prems = _} => mk_mor_UNIV_tac ctxt m morE_thms mor_def)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val timer = time (timer "Morphism definition & thms");
@@ -552,7 +552,7 @@
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies ([prem], concl))
           (fn {context = ctxt, prems = _} => mk_bd_limit_tac ctxt n suc_bd_Cinfinite)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val timer = time (timer "Bounds");
@@ -592,7 +592,7 @@
 
         val min_algs_thm = Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_min_algs_tac ctxt suc_bd_worel in_cong'_thms)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         val min_algs_thms = map (fn k => min_algs_thm RS mk_nthI n k) ks;
 
@@ -604,7 +604,7 @@
             Variable.add_free_names lthy goal []
             |> (fn vars => Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} => mk_min_algs_mono_tac ctxt min_algs))
-            |> Thm.close_derivation)
+            |> Thm.close_derivation \<^here>)
           (map mk_mono_goal min_algss) min_algs_thms;
 
         fun mk_card_conjunct min_alg = mk_ordLeq (mk_card_of min_alg) Asuc_bd;
@@ -622,7 +622,7 @@
                 m suc_bd_worel min_algs_thms in_sbds
                 sbd_Card_order sbd_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero
                 suc_bd_Asuc_bd Asuc_bd_Cinfinite)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
@@ -639,7 +639,7 @@
             Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} => mk_min_algs_least_tac ctxt least_cT least_ct
                 suc_bd_worel min_algs_thms alg_set_thms)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
       in
         (min_algs_thms, monos, card_of, least)
@@ -698,7 +698,7 @@
             Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} => mk_alg_min_alg_tac ctxt m alg_def min_alg_defs
                 suc_bd_limit_thm sbd_Cinfinite set_sbdss min_algs_thms min_algs_mono_thms)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         fun mk_card_of_thm min_alg def =
@@ -709,7 +709,7 @@
             Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} => mk_card_of_min_alg_tac ctxt def card_of_min_algs_thm
                 suc_bd_Card_order suc_bd_Asuc_bd Asuc_bd_Cinfinite)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         fun mk_least_thm min_alg B def =
@@ -720,7 +720,7 @@
           in
             Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} => mk_least_min_alg_tac ctxt def least_min_algs_thm)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val leasts = @{map 3} mk_least_thm min_algs Bs min_alg_defs;
@@ -735,7 +735,7 @@
             Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} =>
                 EVERY' (rtac ctxt mor_incl_thm :: map (etac ctxt) leasts) 1)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
       in
         (alg_min_alg, map2 mk_card_of_thm min_algs min_alg_defs, leasts, incl)
@@ -830,7 +830,7 @@
       (HOLogic.mk_Trueprop (mk_Ball II
         (Term.absfree iidx' (mk_alg select_Bs select_ss))))
       (fn {context = ctxt, prems = _} => mk_alg_select_tac ctxt Abs_IIT_inverse_thm)
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
 
     val mor_select_thm =
       let
@@ -846,7 +846,7 @@
           (fn {context = ctxt, prems = _} => mk_mor_select_tac ctxt mor_def mor_cong_thm
             mor_comp_thm mor_incl_min_alg_thm alg_def alg_select_thm alg_set_thms set_mapss
             str_init_defs)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val init_unique_mor_thms =
@@ -865,7 +865,7 @@
           Goal.prove_sorry lthy vars [] (Logic.list_implies (all_prems, unique))
             (fn {context = ctxt, prems = _} => mk_init_unique_mor_tac ctxt cts m alg_def
               alg_init_thm least_min_alg_thms in_mono'_thms alg_set_thms morE_thms map_cong0s)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         split_conj_thm unique_mor
       end;
@@ -899,7 +899,7 @@
         Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, concl))
           (fn {context = ctxt, prems = _} => mk_init_induct_tac ctxt m alg_def alg_init_thm
             least_min_alg_thms alg_set_thms)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val timer = time (timer "Initiality definition & thms");
@@ -977,7 +977,7 @@
             (HOLogic.mk_Trueprop (mk_mor UNIVs ctors car_inits str_inits Rep_Ts))
             (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt m defs Reps Abs_inverses
               alg_min_alg_thm alg_set_thms set_mapss)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         fun mk_ct initFT str abs = Term.absdummy initFT (abs $ (str $ Bound 0))
         val cts = @{map 3} (Thm.cterm_of lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
@@ -987,7 +987,7 @@
             (HOLogic.mk_Trueprop (mk_mor car_inits str_inits UNIVs ctors Abs_Ts))
             (fn {context = ctxt, prems = _} => mk_mor_Abs_tac ctxt cts defs Abs_inverses
               map_comp_id_thms map_cong0L_thms)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         (mor_Rep, mor_Abs)
       end;
@@ -1046,7 +1046,7 @@
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
           (fn {context = ctxt, prems = _} => mk_copy_tac ctxt m alg_def mor_def alg_set_thms
             set_mapss)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val init_ex_mor_thm =
@@ -1059,7 +1059,7 @@
           (fn {context = ctxt, prems = _} =>
             mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm (alg_min_alg_thm RS copy_thm)
               card_of_min_alg_thms mor_Rep_thm mor_comp_thm mor_select_thm mor_incl_thm)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val mor_fold_thm =
@@ -1073,7 +1073,7 @@
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, ...} =>
             mk_mor_fold_tac ctxt cT ct fold_defs init_ex_mor_thm mor_cong)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val ctor_fold_thms = map (fn morE => rule_by_tactic lthy
@@ -1089,7 +1089,7 @@
         val unique_mor = Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique))
           (fn {context = ctxt, prems = _} => mk_fold_unique_mor_tac ctxt type_defs
             init_unique_mor_thms Reps mor_comp_thm mor_Abs_thm mor_fold_thm)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         `split_conj_thm unique_mor
       end;
@@ -1148,7 +1148,7 @@
           Goal.prove_sorry lthy [] [] goal
             (fn {context = ctxt, prems = _} => mk_dtor_o_ctor_tac ctxt dtor_def foldx map_comp_id
               map_cong0L ctor_o_fold_thms)
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         goals dtor_defs ctor_fold_thms map_comp_id_thms map_cong0L_thms
       end;
 
@@ -1215,7 +1215,7 @@
           (fn {context = ctxt, prems = _} =>
             mk_ctor_induct_tac ctxt m set_mapss init_induct_thm morE_thms mor_Abs_thm
             Rep_inverses Abs_inverses Reps)
-        |> Thm.close_derivation,
+        |> Thm.close_derivation \<^here>,
         rev (Term.add_tfrees goal []))
       end;
 
@@ -1258,7 +1258,7 @@
         (Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_ctor_induct2_tac ctxt cTs cts ctor_induct_thm
             weak_ctor_induct_thms)
-        |> Thm.close_derivation,
+        |> Thm.close_derivation \<^here>,
         rev (Term.add_tfrees goal []))
       end;
 
@@ -1495,7 +1495,7 @@
                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
                     mk_map_tac ctxt m n foldx map_comp_id map_cong0))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               goals ctor_fold_thms map_comp_id_thms map_cong0s;
           in
             `(map (fn thm => thm RS @{thm comp_eq_dest})) maps
@@ -1514,7 +1514,7 @@
             val unique = Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal))
               (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
                 mk_ctor_map_unique_tac ctxt ctor_fold_unique_thm sym_map_comps)
-              |> Thm.close_derivation;
+              |> Thm.close_derivation \<^here>;
           in
             `split_conj_thm unique
           end;
@@ -1532,7 +1532,7 @@
             val setss = map (map2 (fn foldx => fn goal =>
                 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
                   unfold_thms_tac ctxt Iset_defs THEN mk_set_tac ctxt foldx)
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               ctor_fold_thms) goalss;
 
             fun mk_simp_goal pas_set act_sets sets ctor z set =
@@ -1550,7 +1550,7 @@
               |> (fn vars => Goal.prove_sorry lthy vars [] goal
                   (fn {context = ctxt, prems = _} =>
                     mk_ctor_set_tac ctxt set (nth set_nats (i - 1)) (drop m set_nats)))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               set_mapss) ls simp_goalss setss;
           in
             ctor_setss
@@ -1597,7 +1597,7 @@
                 Variable.add_free_names lthy goal []
                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
                   (fn {context = ctxt, prems = _} => mk_tac ctxt induct csets ctor_sets i))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               goals csetss ctor_Iset_thmss inducts ls;
           in
             map split_conj_thm thms
@@ -1626,7 +1626,7 @@
                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
                     (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Ibd_defs THEN
                       mk_tac ctxt induct ctor_sets i))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               goals ctor_Iset_thmss inducts ls;
           in
             map split_conj_thm thms
@@ -1657,7 +1657,7 @@
             val thm = Goal.prove_sorry lthy vars [] goal
                 (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt (rtac ctxt induct) set_Iset_thmsss
                   map_cong0s ctor_Imap_thms)
-              |> Thm.close_derivation;
+              |> Thm.close_derivation \<^here>;
           in
             split_conj_thm thm
           end;
@@ -1693,7 +1693,7 @@
                (fn {context = ctxt, prems = _} =>
                  mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets
                    ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss))
-              |> Thm.close_derivation)
+              |> Thm.close_derivation \<^here>)
             ks goals in_rels map_comps map_cong0s ctor_Imap_thms ctor_Iset_thmss'
               ctor_inject_thms ctor_dtor_thms set_mapss ctor_Iset_incl_thmss
               ctor_set_Iset_incl_thmsss
@@ -1718,7 +1718,7 @@
             Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms
                 ctor_Irel_thms rel_mono_strong0s le_rel_OOs)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val timer = time (timer "helpers for BNF properties");
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -158,7 +158,7 @@
 
     fun prove goal =
       Goal.prove_sorry ctxt [] [] goal (tac o #context)
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
   in
     map (map prove) goalss
   end;
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_lfp_countable.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_countable.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -178,7 +178,7 @@
           inj_map_strongs')
       |> HOLogic.conj_elims ctxt
       |> Proof_Context.export names_ctxt ctxt
-      |> map Thm.close_derivation
+      |> map (Thm.close_derivation \<^here>)
     end;
 
 fun get_countable_goal_type_name (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>Ex\<close>, _)
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -557,7 +557,7 @@
                 (fn {context = ctxt, prems = _} =>
                   mk_primrec_tac ctxt num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
                     fp_nesting_pred_maps def_thms rec_thm)
-              |> Thm.close_derivation);
+              |> Thm.close_derivation \<^here>);
       in
         ((js, simps), lthy')
       end;
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -300,7 +300,7 @@
                 mk_size_neq ctxt (map (Thm.cterm_of lthy2) xs)
                 (#exhaust (#ctr_sugar (#fp_ctr_sugar fp_sugar))) size_thms)
               |> single
-              |> map Thm.close_derivation;
+              |> map (Thm.close_derivation \<^here>);
           in thm end) fp_sugars overloaded_size_consts overloaded_size_simpss;
 
       val ABs = As ~~ Bs;
@@ -347,7 +347,7 @@
                 @{map 3} (fn goal => fn size_def => fn rec_o_map =>
                     Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
                       mk_size_gen_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps)
-                    |> Thm.close_derivation
+                    |> Thm.close_derivation \<^here>
                     |> single)
                   size_gen_o_map_goals size_defs rec_o_maps
               else
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/BNF/bnf_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_tactics.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -59,7 +59,7 @@
     (K (rtac ctxt ext 1 THEN
         unfold_thms_tac ctxt ([o_apply, unfold_thms ctxt [o_apply] (mk_sym thm)]) THEN
         rtac ctxt refl 1)))
-  |> Thm.close_derivation;
+  |> Thm.close_derivation \<^here>;
 
 
 (* Theorems for open typedefs with UNIV as representing set *)
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -731,7 +731,7 @@
           in
             Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
               mk_nchotomy_tac ctxt n exhaust_thm)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val case_thms =
@@ -743,7 +743,7 @@
             @{map 4} (fn k => fn goal => fn injects => fn distinctss =>
                 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
                   mk_case_tac ctxt n k case_def injects distinctss)
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               ks goals inject_thmss distinct_thmsss
           end;
 
@@ -764,7 +764,7 @@
                mk_case_cong_tac ctxt uexhaust_thm case_thms),
              Goal.prove_sorry lthy weak_vars [] weak_goal (fn {context = ctxt, prems = _} =>
                etac ctxt arg_cong 1))
-            |> apply2 (Thm.close_derivation)
+            |> apply2 (Thm.close_derivation \<^here>)
           end;
 
         val split_lhs = q $ ufcase;
@@ -786,13 +786,13 @@
           Variable.add_free_names lthy goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
             mk_split_tac ctxt uexhaust_thm case_thms selss inject_thmss distinct_thmsss))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         fun prove_split_asm asm_goal split_thm =
           Variable.add_free_names lthy asm_goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] asm_goal (fn {context = ctxt, ...} =>
             mk_split_asm_tac ctxt split_thm))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         val (split_thm, split_asm_thm) =
           let
@@ -851,7 +851,7 @@
                 in
                   Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
                     mk_unique_disc_def_tac ctxt m uexhaust_thm)
-                  |> Thm.close_derivation
+                  |> Thm.close_derivation \<^here>
                 end;
 
               fun mk_alternate_disc_def k =
@@ -864,7 +864,7 @@
                   Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
                     mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
                       (nth distinct_thms (2 - k)) uexhaust_thm)
-                  |> Thm.close_derivation
+                  |> Thm.close_derivation \<^here>
                 end;
 
               val has_alternate_disc_def =
@@ -917,7 +917,7 @@
 
                   fun prove tac goal =
                     Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => tac ctxt)
-                    |> Thm.close_derivation;
+                    |> Thm.close_derivation \<^here>;
 
                   val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs));
 
@@ -945,7 +945,7 @@
                 in
                   Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
                     mk_exhaust_disc_tac ctxt n exhaust_thm discI_thms)
-                  |> Thm.close_derivation
+                  |> Thm.close_derivation \<^here>
                 end;
 
               val (safe_collapse_thms, all_collapse_thms) =
@@ -962,7 +962,7 @@
                     @{map 5} (fn m => fn discD => fn sel_thms => fn triv => fn goal =>
                         Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
                           mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL (assume_tac ctxt))
-                        |> Thm.close_derivation
+                        |> Thm.close_derivation \<^here>
                         |> not triv ? perhaps (try (fn thm => refl RS thm)))
                       ms discD_thms sel_thmss trivs goals;
                 in
@@ -980,7 +980,7 @@
                 in
                   Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
                     mk_exhaust_sel_tac ctxt n exhaust_disc_thm swapped_all_collapse_thms)
-                  |> Thm.close_derivation
+                  |> Thm.close_derivation \<^here>
                 end;
 
               val expand_thm =
@@ -1006,7 +1006,7 @@
                     mk_expand_tac ctxt n ms (inst_thm u exhaust_disc_thm)
                       (inst_thm v exhaust_disc_thm) uncollapse_thms distinct_disc_thmsss
                       distinct_disc_thmsss')
-                  |> Thm.close_derivation
+                  |> Thm.close_derivation \<^here>
                 end;
 
               val (split_sel_thm, split_sel_asm_thm) =
@@ -1028,7 +1028,7 @@
                 in
                   Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
                     mk_case_eq_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
-                  |> Thm.close_derivation
+                  |> Thm.close_derivation \<^here>
                 end;
 
               val disc_eq_case_thms =
@@ -1044,7 +1044,7 @@
                   Goal.prove_sorry lthy vars [] goal
                     (fn {context = ctxt, ...} => mk_disc_eq_case_tac ctxt (Thm.cterm_of ctxt u)
                        exhaust_thm (flat nontriv_disc_thmss) distinct_thms case_thms)
-                  |> Thm.close_derivation
+                  |> Thm.close_derivation \<^here>
                   |> Conjunction.elim_balanced (length goals)
                 end;
             in
@@ -1066,7 +1066,7 @@
           in
             Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
               mk_case_distrib_tac ctxt (Thm.cterm_of ctxt u) exhaust_thm case_thms)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
@@ -1151,7 +1151,7 @@
   end;
 
 fun free_constructors kind tacss = (fn (goalss, after_qed, lthy) =>
-  map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss
+  map2 (map2 (Thm.close_derivation \<^here> oo Goal.prove_sorry lthy [] [])) goalss tacss
   |> (fn thms => after_qed thms lthy)) oo prepare_free_constructors kind (K I) (K I);
 
 fun free_constructors_cmd kind = (fn (goalss, after_qed, lthy) =>
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -76,7 +76,7 @@
     fun proves goals = goals
       |> Logic.mk_conjunction_balanced
       |> prove
-      |> Thm.close_derivation
+      |> Thm.close_derivation \<^here>
       |> Conjunction.elim_balanced (length goals)
       |> map Simpdata.mk_eq;
   in
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -221,11 +221,13 @@
 fun name_noted_thms _ _ [] = []
   | name_noted_thms qualifier base ((local_name, thms) :: noted) =
     if Long_Name.base_name local_name = base then
-      (local_name,
-       map_index (uncurry (fn j => Thm.name_derivation (Long_Name.append qualifier base ^
-         (if can the_single thms then "" else "_" ^ string_of_int (j + 1))))) thms) :: noted
-    else
-      ((local_name, thms) :: name_noted_thms qualifier base noted);
+      let
+        val thms' = thms |> map_index (uncurry (fn j =>
+          Thm.name_derivation
+            (((Long_Name.append qualifier base ^
+              (if can the_single thms then "" else "_" ^ string_of_int (j + 1))), Position.none))))
+      in (local_name, thms') :: noted end
+    else ((local_name, thms) :: name_noted_thms qualifier base noted);
 
 fun substitute_noted_thm noted =
   let val tab = fold (fold (Termtab.default o `Thm.full_prop_of) o snd) noted Termtab.empty in
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Function/function.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -90,7 +90,7 @@
 
     fun afterqed [[proof]] lthy =
       let
-        val result = cont lthy (Thm.close_derivation proof)
+        val result = cont lthy (Thm.close_derivation \<^here> proof)
         val FunctionResult {fs, R, dom, psimps, simple_pinducts,
                 termination, domintros, cases, ...} = result
 
@@ -185,7 +185,7 @@
     val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
     fun afterqed [[totality]] lthy =
       let
-        val totality = Thm.close_derivation totality
+        val totality = Thm.close_derivation \<^here> totality
         val remove_domain_condition =
           full_simplify (put_simpset HOL_basic_ss lthy
             addsimps [totality, @{thm True_implies_equals}])
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -275,7 +275,7 @@
       |> fold_rev (Thm.implies_intr o Thm.cprop_of) h_assums
       |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
       |> fold_rev Thm.forall_intr cqs
-      |> Thm.close_derivation
+      |> Thm.close_derivation \<^here>
   in
     replace_lemma
   end
@@ -426,7 +426,7 @@
             (Term.add_vars (Thm.prop_of it) []) it)
 
     val goalstate =  Conjunction.intr graph_is_function complete
-      |> Thm.close_derivation
+      |> Thm.close_derivation \<^here>
       |> Goal.protect 0
       |> fold_rev (Thm.implies_intr o Thm.cprop_of) compat
       |> Thm.implies_intr (Thm.cprop_of complete)
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/Lifting/lifting_bnf.ML
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -67,7 +67,7 @@
   in
     Goal.prove_sorry ctxt'' [] [] goal
       (fn {context = goal_ctxt, ...} => Quotient_tac bnf goal_ctxt 1)
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
     |> singleton (Variable.export ctxt'' ctxt)
     |> Drule.zero_var_indexes
   end
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -664,7 +664,7 @@
         let
           val rsp_thm =
             Goal.prove_sorry lthy [] [] goal (tac o #context)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
         in
           after_qed rsp_thm lthy
         end
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -288,7 +288,7 @@
             val f'_rsp = Goal.prove_sorry lthy3 [] [] f'_rsp_goal
               (fn {context = ctxt, prems = _} =>
                 HEADGOAL (CONVERSION (rel_eq_onps_conv) THEN' rtac ctxt rsp_norm))
-              |> Thm.close_derivation
+              |> Thm.close_derivation \<^here>
             val (f'_lift_def, lthy4) = add_lift_def ld_no_notes f'_var f'_qty rhs f'_rsp [] lthy3
             val f'_lift_def = inst_of_lift_def lthy4 f'_qty f'_lift_def
             val f'_lift_const = mk_lift_const_of_lift_def f'_qty f'_lift_def
@@ -306,7 +306,7 @@
             val f_alt_def =
               Goal.prove_sorry transfer_ctxt [] [] f_alt_def_goal
                 (fn {context = goal_ctxt, ...} => HEADGOAL (f_alt_def_tac goal_ctxt))
-              |> Thm.close_derivation
+              |> Thm.close_derivation \<^here>
               |> singleton (Variable.export transfer_ctxt lthy4)
             val lthy5 = lthy4
               |> Local_Theory.note ((Binding.empty, @{attributes [code]}), [f_alt_def])
@@ -458,7 +458,7 @@
     val quot_thm_isom =
       Goal.prove_sorry transfer_ctxt [] [] typedef_goal
         (fn {context = goal_ctxt, ...} => typ_isom_tac goal_ctxt 1)
-      |> Thm.close_derivation
+      |> Thm.close_derivation \<^here>
       |> singleton (Variable.export transfer_ctxt lthy6)
       |> (fn thm => @{thm UNIV_typedef_to_Quotient} OF [thm, @{thm reflexive}])
     val qty_isom_name = Tname qty_isom;
@@ -540,7 +540,7 @@
     val rep_isom_code =
       Goal.prove_sorry x_ctxt [] [] rep_isom_code_goal
         (fn {context = goal_ctxt, ...} => rep_isom_code_tac ctr_sugar goal_ctxt 1)
-      |> Thm.close_derivation
+      |> Thm.close_derivation \<^here>
       |> singleton(Variable.export x_ctxt lthy6)
   in
     lthy6
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -384,7 +384,7 @@
                      #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
              |> Variable.export ctxt2 ctxt0
              |> finish_cnf
-             |> map Thm.close_derivation)
+             |> map (Thm.close_derivation \<^here>))
   end
   handle THM _ => (NONE, [])
 
diff -r a9053fa30909 -r 41108e3e9ca5 src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -93,7 +93,7 @@
   in
     Goal.prove_sorry ctxt' [] [] goal (fn {context = goal_ctxt, ...} =>
       side_constraint_tac bnf [constraint_def] goal_ctxt 1)
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
     |> singleton (Variable.export ctxt' ctxt)
     |> Drule.zero_var_indexes
   end
@@ -104,7 +104,7 @@
   in
     Goal.prove_sorry ctxt' [] [] goal (fn {context = goal_ctxt, ...} =>
       bi_constraint_tac constraint_def side_constraints goal_ctxt 1)
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
     |> singleton (Variable.export ctxt' ctxt)
     |> Drule.zero_var_indexes
   end
@@ -189,7 +189,7 @@
   in
     Goal.prove_sorry ctxt'' [] [] goal (fn {context = goal_ctxt, ...} =>
       Domainp_tac bnf pred_def goal_ctxt 1)
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
     |> singleton (Variable.export ctxt'' ctxt)
     |> Drule.zero_var_indexes
   end
diff -r a9053fa30909 -r 41108e3e9ca5 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/General/binding.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -18,6 +18,7 @@
   val set_pos: Position.T -> binding -> binding
   val reset_pos: binding -> binding
   val default_pos: binding -> binding
+  val default_pos_of: binding -> Position.T
   val name: bstring -> binding
   val name_of: binding -> bstring
   val map_name: (bstring -> bstring) -> binding -> binding
@@ -95,6 +96,10 @@
 fun default_pos b =
   if pos_of b = Position.none then set_pos (Position.thread_data ()) b else b;
 
+fun default_pos_of b =
+  let val pos = pos_of b
+  in if pos = Position.none then Position.thread_data () else pos end;
+
 
 (* name *)
 
diff -r a9053fa30909 -r 41108e3e9ca5 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/Isar/code.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -90,11 +90,6 @@
 
 (** auxiliary **)
 
-(* close theorem for storage *)
-
-val close = Thm.trim_context o Thm.close_derivation;
-
-
 (* printing *)
 
 fun string_of_typ thy =
@@ -1012,13 +1007,13 @@
       Abstract (snd (constrain_thm thy (fst (typscheme_abs thy abs_thm)) sorts abs_thm), tyco);
 
 fun conclude_cert (Nothing cert_thm) =
-      Nothing (Thm.close_derivation cert_thm)
+      Nothing (Thm.close_derivation \<^here> cert_thm)
   | conclude_cert (Equations (cert_thm, propers)) =
-      Equations (Thm.close_derivation cert_thm, propers)
+      Equations (Thm.close_derivation \<^here> cert_thm, propers)
   | conclude_cert (cert as Projection _) =
       cert
   | conclude_cert (Abstract (abs_thm, tyco)) =
-      Abstract (Thm.close_derivation abs_thm, tyco);
+      Abstract (Thm.close_derivation \<^here> abs_thm, tyco);
 
 fun typscheme_of_cert thy (Nothing cert_thm) =
       fst (get_head thy cert_thm)
@@ -1403,7 +1398,7 @@
         (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^
             Thm.string_of_thm_global thy thm') else (); true)
       else false;
-  in (close thm, proper) :: filter_out drop eqns end;
+  in (thm |> Thm.close_derivation \<^here> |> Thm.trim_context, proper) :: filter_out drop eqns end;
 
 fun add_eqn_for (c, eqn) thy =
   thy |> modify_specs (modify_pending_eqns c (subsumptive_add thy true eqn));
@@ -1419,7 +1414,7 @@
     else specs);
 
 fun add_abstract_for (c, (thm, tyco_abs as (tyco, _))) =
-  modify_specs (register_fun_spec c (Abstr (Thm.close_derivation thm, tyco_abs))
+  modify_specs (register_fun_spec c (Abstr (Thm.close_derivation \<^here> thm, tyco_abs))
     #> map_types (History.modify_entry tyco (add_abstract_function c)))
 
 in
diff -r a9053fa30909 -r 41108e3e9ca5 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
diff -r a9053fa30909 -r 41108e3e9ca5 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/Isar/generic_target.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -303,13 +303,16 @@
 
   in (result'', result) end;
 
+fun bind_name lthy b =
+  (Local_Theory.full_name lthy b, Binding.default_pos_of b);
+
 in
 
 fun notes target_notes kind facts lthy =
   let
     val facts' = facts
-      |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
-          (Local_Theory.full_name lthy (fst a))) bs))
+      |> map (fn (a, bs) =>
+          (a, Global_Theory.burrow_fact (Global_Theory.name_multi (bind_name lthy (fst a))) bs))
       |> Global_Theory.map_facts (import_export_proof lthy);
     val local_facts = Global_Theory.map_facts #1 facts';
     val global_facts = Global_Theory.map_facts #2 facts';
diff -r a9053fa30909 -r 41108e3e9ca5 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -497,7 +497,7 @@
     fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal);
 
     val th =
-      (Goal.conclude (Thm.close_derivation goal) handle THM _ => err_lost ())
+      (Goal.conclude (Thm.close_derivation \<^here> goal) handle THM _ => err_lost ())
       |> Drule.flexflex_unique (SOME ctxt)
       |> Thm.check_shyps ctxt
       |> Thm.check_hyps (Context.Proof ctxt);
diff -r a9053fa30909 -r 41108e3e9ca5 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -1074,27 +1074,29 @@
 fun update_facts flags (b, SOME ths) ctxt = ctxt |> add_facts flags (b, Lazy.value ths) |> #2
   | update_facts _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b));
 
+fun bind_name ctxt b = (full_name ctxt b, Binding.default_pos_of b);
+
 in
 
 fun add_thms_lazy kind (b, ths) ctxt =
   let
-    val name = full_name ctxt b;
+    val name_pos = bind_name ctxt b;
     val ths' =
       Global_Theory.check_thms_lazy ths
       |> Lazy.map_finished
-          (Global_Theory.name_thms Global_Theory.unofficial1 name #> map (Thm.kind_rule kind));
+          (Global_Theory.name_thms Global_Theory.unofficial1 name_pos #> map (Thm.kind_rule kind));
     val (_, ctxt') = add_facts {index = is_stmt ctxt} (b, ths') ctxt;
   in ctxt' end;
 
 fun note_thms kind ((b, more_atts), facts) ctxt =
   let
-    val name = full_name ctxt b;
+    val (name, pos) = bind_name ctxt b;
     val facts' = facts
-      |> Global_Theory.burrow_fact (Global_Theory.name_thms Global_Theory.unofficial1 name);
+      |> Global_Theory.burrow_fact (Global_Theory.name_thms Global_Theory.unofficial1 (name, pos));
     fun app (ths, atts) =
       fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
     val (res, ctxt') = fold_map app facts' ctxt;
-    val thms = Global_Theory.name_thms Global_Theory.unofficial2 name (flat res);
+    val thms = Global_Theory.name_thms Global_Theory.unofficial2 (name, pos) (flat res);
     val (_, ctxt'') = ctxt' |> add_facts {index = is_stmt ctxt} (b, Lazy.value thms);
   in ((name, thms), ctxt'') end;
 
diff -r a9053fa30909 -r 41108e3e9ca5 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/ML/ml_thms.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -91,7 +91,7 @@
         val _ = Context_Position.reports ctxt reports;
 
         val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
-        val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;
+        val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation \<^here>;
         fun after_qed res goal_ctxt =
           Proof_Context.put_thms false (Auto_Bind.thisN,
             SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
diff -r a9053fa30909 -r 41108e3e9ca5 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -595,8 +595,9 @@
               (corr_prf1 % u %% corr_prf2, defs2)
           end
 
-      | corr d vs ts Ts hs cs _ (prf0 as PThm ({name, prop, types = SOME Ts', ...}, thm_body)) _ defs =
+      | corr d vs ts Ts hs cs _ (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) _ defs =
           let
+            val {pos, name, prop, ...} = thm_header;
             val prf = Proofterm.thm_body_proof_open thm_body;
             val (vs', tye) = find_inst prop Ts ts vs;
             val shyps = mk_shyps tye;
@@ -621,7 +622,7 @@
                     val corr_prf = mkabsp shyps corr_prf0;
                     val corr_prop = Proofterm.prop_of corr_prf;
                     val corr_header =
-                      Proofterm.thm_header (Proofterm.proof_serial ()) (corr_name name vs')
+                      Proofterm.thm_header (Proofterm.proof_serial ()) pos (corr_name name vs')
                         corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
                     val corr_body =
                       Proofterm.thm_body I (Future.value (Proofterm.approximate_proof_body corr_prf));
@@ -696,8 +697,9 @@
               in (f $ t, defs'') end
           end
 
-      | extr d vs ts Ts hs (prf0 as PThm ({name = s, prop, types = SOME Ts', ...}, thm_body)) defs =
+      | extr d vs ts Ts hs (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) defs =
           let
+            val {pos, name = s, prop, ...} = thm_header;
             val prf = Proofterm.thm_body_proof_open thm_body;
             val (vs', tye) = find_inst prop Ts ts vs;
             val shyps = mk_shyps tye;
@@ -741,7 +743,7 @@
                              SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
                     val corr_prop = Proofterm.prop_of corr_prf';
                     val corr_header =
-                      Proofterm.thm_header (Proofterm.proof_serial ()) (corr_name s vs')
+                      Proofterm.thm_header (Proofterm.proof_serial ()) pos (corr_name s vs')
                         corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
                     val corr_body =
                       Proofterm.thm_body I
diff -r a9053fa30909 -r 41108e3e9ca5 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/drule.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -256,7 +256,7 @@
 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*)
diff -r a9053fa30909 -r 41108e3e9ca5 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/global_theory.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -20,15 +20,15 @@
   val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
   val burrow_facts: ('a list -> 'b list) ->
     ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
-  val name_multi: string -> 'a list -> (string * 'a) list
+  val name_multi: string * Position.T -> 'a list -> ((string * Position.T) * 'a) list
   type name_flags
   val unnamed: name_flags
   val official1: name_flags
   val official2: name_flags
   val unofficial1: name_flags
   val unofficial2: name_flags
-  val name_thm: name_flags -> string -> thm -> thm
-  val name_thms: name_flags -> string -> thm list -> thm list
+  val name_thm: name_flags -> string * Position.T -> thm -> thm
+  val name_thms: name_flags -> string * Position.T -> thm list -> thm list
   val check_thms_lazy: thm list lazy -> thm list lazy
   val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
   val store_thm: binding * thm -> theory -> thm * theory
@@ -122,35 +122,39 @@
 val unofficial1 = Name_Flags {pre = true, official = false};
 val unofficial2 = Name_Flags {pre = false, official = false};
 
-fun name_thm name_flags name =
+fun name_thm name_flags (name, pos) =
   Thm.solve_constraints #> (fn thm =>
     (case name_flags of
       No_Name_Flags => thm
     | Name_Flags {pre, official} =>
         thm
         |> (official andalso (not pre orelse Thm.derivation_name thm = "")) ?
-            Thm.name_derivation name
+            Thm.name_derivation (name, pos)
         |> (name <> "" andalso (not pre orelse not (Thm.has_name_hint thm))) ?
             Thm.put_name_hint name));
 
 end;
 
-fun name_multi name [x] = [(name, x)]
-  | name_multi "" xs = map (pair "") xs
-  | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
+fun name_multi (name, pos: Position.T) xs =
+  (case xs of
+    [x] => [((name, pos), x)]
+  | _ =>
+      if name = "" then map (pair ("", pos)) xs
+      else map_index (fn (i, x) => ((name ^ "_" ^ string_of_int (i + 1), pos), x)) xs);
 
-fun name_thms name_flags name thms =
-  map (uncurry (name_thm name_flags)) (name_multi name thms);
+fun name_thms name_flags name_pos thms =
+  map (uncurry (name_thm name_flags)) (name_multi name_pos thms);
 
 
 (* apply theorems and attributes *)
 
 fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
 
+fun bind_name thy b = (Sign.full_name thy b, Binding.default_pos_of b);
+
 fun add_facts (b, fact) thy =
   let
-    val full_name = Sign.full_name thy b;
-    val pos = Binding.pos_of b;
+    val (full_name, pos) = bind_name thy b;
     fun check fact =
       fact |> map_index (fn (i, thm) =>
         let
@@ -183,10 +187,10 @@
   if Binding.is_empty b then Thm.register_proofs (check_thms_lazy thms) thy
   else
     let
-      val name = Sign.full_name thy b;
+      val name_pos = bind_name thy b;
       val thms' =
         check_thms_lazy thms
-        |> Lazy.map_finished (name_thms official1 name #> map (Thm.kind_rule kind));
+        |> Lazy.map_finished (name_thms official1 name_pos #> map (Thm.kind_rule kind));
     in thy |> Thm.register_proofs thms' |> add_facts (b, thms') end;
 
 val app_facts =
@@ -196,10 +200,10 @@
   if Binding.is_empty b then app_facts facts thy |-> register_proofs
   else
     let
-      val name = Sign.full_name thy b;
+      val name_pos= bind_name thy b;
       val (thms', thy') = thy
-        |> app_facts (map (apfst (name_thms name_flags1 name)) facts)
-        |>> name_thms name_flags2 name |-> register_proofs;
+        |> app_facts (map (apfst (name_thms name_flags1 name_pos)) facts)
+        |>> name_thms name_flags2 name_pos |-> register_proofs;
       val thy'' = thy' |> add_facts (b, Lazy.value thms');
     in (map (Thm.transfer thy'') thms', thy'') end;
 
diff -r a9053fa30909 -r 41108e3e9ca5 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/goal.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -136,7 +136,7 @@
         Thm.solve_constraints);
     val local_result =
       Thm.future global_result global_prop
-      |> Thm.close_derivation
+      |> Thm.close_derivation \<^here>
       |> Thm.instantiate (instT, [])
       |> Drule.forall_elim_list fixes
       |> fold (Thm.elim_implies o Thm.assume) assms
@@ -220,7 +220,7 @@
           (Thm.term_of stmt);
   in
     res
-    |> Thm.close_derivation
+    |> Thm.close_derivation \<^here>
     |> Conjunction.elim_balanced (length props)
     |> map (Assumption.export false ctxt' ctxt)
     |> Variable.export ctxt' ctxt
diff -r a9053fa30909 -r 41108e3e9ca5 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/proofterm.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -11,7 +11,7 @@
   type thm_node
   type proof_serial = int
   type thm_header =
-    {serial: proof_serial, name: string, prop: term, types: typ list option}
+    {serial: proof_serial, pos: Position.T, name: string, prop: term, types: typ list option}
   type thm_body
   datatype proof =
      MinProof
@@ -40,7 +40,7 @@
   type oracle = string * term
   val proof_of: proof_body -> proof
   val map_proof_of: (proof -> proof) -> proof_body -> proof_body
-  val thm_header: proof_serial -> string -> term -> typ list option -> thm_header
+  val thm_header: proof_serial -> Position.T -> string -> term -> typ list option -> thm_header
   val thm_body: (proof -> proof) -> proof_body future -> thm_body
   val thm_body_proof_raw: thm_body -> proof
   val thm_body_proof_open: thm_body -> proof
@@ -165,8 +165,8 @@
   val proof_serial: unit -> proof_serial
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
   val thm_proof: theory -> (class * class -> proof) ->
-    (string * class list list * class -> proof) -> string -> sort list -> term list -> term ->
-    (serial * proof_body future) list -> proof_body -> pthm * proof
+    (string * class list list * class -> proof) -> string * Position.T -> sort list ->
+    term list -> term -> (serial * proof_body future) list -> proof_body -> pthm * proof
   val unconstrain_thm_proof: theory -> (class * class -> proof) ->
     (string * class list list * class -> proof) -> sort list -> term ->
     (serial * proof_body future) list -> proof_body -> pthm * proof
@@ -181,7 +181,7 @@
 type proof_serial = int;
 
 type thm_header =
-  {serial: proof_serial, name: string, prop: term, types: typ list option};
+  {serial: proof_serial, pos: Position.T, name: string, prop: term, types: typ list option};
 
 datatype proof =
    MinProof
@@ -213,8 +213,8 @@
 fun map_proof_of f (PBody {oracles, thms, proof}) =
   PBody {oracles = oracles, thms = thms, proof = f proof};
 
-fun thm_header serial name prop types : thm_header =
-  {serial = serial, name = name, prop = prop, types = types};
+fun thm_header serial pos name prop types : thm_header =
+  {serial = serial, pos = pos, name = name, prop = prop, types = types};
 
 fun thm_body open_proof body =
   Thm_Body {open_proof = open_proof, body = body};
@@ -369,9 +369,10 @@
   fn PAxm (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
   fn OfClass (a, b) => ([b], typ a),
   fn Oracle (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
-  fn PThm ({serial, name, prop, types}, Thm_Body {open_proof, body}) =>
-    ([int_atom serial, name], triple term (option (list typ)) proof_body
-      (prop, types, map_proof_of open_proof (Future.join body)))]
+  fn PThm ({serial, pos, name, prop, types}, Thm_Body {open_proof, body}) =>
+    ([int_atom serial, name],
+      pair properties (pair term (pair (option (list typ)) proof_body))
+        (Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))]
 and proof_body (PBody {oracles, thms, proof = prf}) =
   triple (list (pair string term)) (list pthm) proof (oracles, thms, prf)
 and pthm (a, thm_node) =
@@ -404,8 +405,8 @@
   fn ([b], a) => OfClass (typ a, b),
   fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in Oracle (a, c, d) end,
   fn ([a, b], c) =>
-    let val (d, e, f) = triple term (option (list typ)) proof_body c
-    in PThm (thm_header (int_atom a) b d e, thm_body I (Future.value f)) end]
+    let val ((d, (e, (f, g)))) = pair properties (pair term (pair (option (list typ)) proof_body)) c
+    in PThm (thm_header (int_atom a) (Position.of_properties d) b e f, thm_body I (Future.value g)) end]
 and proof_body x =
   let val (a, b, c) = triple (list (pair string term)) (list pthm) proof x
   in PBody {oracles = a, thms = b, proof = c} end
@@ -479,8 +480,8 @@
       | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
       | proof (OfClass T_c) = ofclass T_c
       | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
-      | proof (PThm ({serial, name, prop, types = SOME Ts}, thm_body)) =
-          PThm (thm_header serial name prop (SOME (typs Ts)), thm_body)
+      | proof (PThm ({serial, pos, name, prop, types = SOME Ts}, thm_body)) =
+          PThm (thm_header serial pos name prop (SOME (typs Ts)), thm_body)
       | proof _ = raise Same.SAME;
   in proof end;
 
@@ -519,8 +520,8 @@
 fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
   | change_types (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
   | change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)
-  | change_types types (PThm ({serial, name, prop, ...}, thm_body)) =
-      PThm (thm_header serial name prop types, thm_body)
+  | change_types types (PThm ({serial, pos, name, prop, types = _}, thm_body)) =
+      PThm (thm_header serial pos name prop types, thm_body)
   | change_types _ prf = prf;
 
 
@@ -667,8 +668,8 @@
           OfClass (htypeT Envir.norm_type_same T, c)
       | norm (Oracle (s, prop, Ts)) =
           Oracle (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
-      | norm (PThm ({serial = i, name = a, prop = t, types = Ts}, thm_body)) =
-          PThm (thm_header i a t (Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body)
+      | norm (PThm ({serial = i, pos = p, name = a, prop = t, types = Ts}, thm_body)) =
+          PThm (thm_header i p a t (Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body)
       | norm _ = raise Same.SAME;
   in Same.commit norm end;
 
@@ -992,8 +993,8 @@
           OfClass (Logic.incr_tvar_same inc T, c)
       | lift' _ _ (Oracle (s, prop, Ts)) =
           Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
-      | lift' _ _ (PThm ({serial = i, name = s, prop, types = Ts}, thm_body)) =
-          PThm (thm_header i s prop ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts),
+      | lift' _ _ (PThm ({serial = i, pos = p, name = s, prop, types = Ts}, thm_body)) =
+          PThm (thm_header i p s prop ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts),
             thm_body)
       | lift' _ _ _ = raise Same.SAME
     and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf);
@@ -1423,8 +1424,8 @@
       | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
       | subst _ _ (OfClass (T, c)) = OfClass (substT T, c)
       | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
-      | subst _ _ (PThm ({serial = i, name = id, prop, types}, thm_body)) =
-          PThm (thm_header i id prop (Same.map_option substTs types), thm_body)
+      | subst _ _ (PThm ({serial = i, pos = p, name = id, prop, types}, thm_body)) =
+          PThm (thm_header i p id prop (Same.map_option substTs types), thm_body)
       | subst _ _ _ = raise Same.SAME;
   in fn t => subst 0 0 t handle Same.SAME => t end;
 
@@ -2038,7 +2039,7 @@
   else proof;
 
 fun prepare_thm_proof unconstrain thy classrel_proof arity_proof
-    name shyps hyps concl promises body =
+    (name, pos) shyps hyps concl promises body =
   let
     val named = name <> "";
 
@@ -2067,7 +2068,7 @@
     val (i, body') =
       (*non-deterministic, depends on unknown promises*)
       (case strip_combt (fst (strip_combP prf)) of
-        (PThm ({serial = i, name = a, prop = prop', types = NONE}, thm_body'), args') =>
+        (PThm ({serial = i, name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
           if (a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then
             let val Thm_Body {body = body', ...} = thm_body';
             in (i, body' |> (a = "" andalso named) ? Future.map (publish i)) end
@@ -2076,7 +2077,7 @@
 
     val pthm = (i, make_thm_node name prop1 body');
 
-    val head = PThm (thm_header i name prop1 NONE, thm_body open_proof body');
+    val head = PThm (thm_header i pos name prop1 NONE, thm_body open_proof body');
     val proof =
       if unconstrain then
         proof_combt' (head, (map o Option.map o Term.map_types) (#map_atyps ucontext) args)
@@ -2090,7 +2091,8 @@
 val thm_proof = prepare_thm_proof false;
 
 fun unconstrain_thm_proof thy classrel_proof arity_proof shyps concl promises body =
-  prepare_thm_proof true thy classrel_proof arity_proof "" shyps [] concl promises body;
+  prepare_thm_proof true thy classrel_proof arity_proof ("", Position.none)
+    shyps [] concl promises body;
 
 end;
 
diff -r a9053fa30909 -r 41108e3e9ca5 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Aug 09 15:58:26 2019 +0200
+++ b/src/Pure/thm.ML	Fri Aug 09 17:14:49 2019 +0200
@@ -106,8 +106,8 @@
   val future: thm future -> cterm -> thm
   val derivation_closed: thm -> bool
   val derivation_name: thm -> string
-  val name_derivation: string -> thm -> thm
-  val close_derivation: thm -> thm
+  val name_derivation: string * Position.T -> thm -> thm
+  val close_derivation: Position.T -> thm -> thm
   val trim_context: thm -> thm
   val axiom: theory -> string -> thm
   val axioms_of: theory -> (string * thm) list
@@ -1000,7 +1000,7 @@
 fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
   Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);
 
-fun name_derivation name =
+fun name_derivation name_pos =
   solve_constraints #> (fn thm as Thm (der, args) =>
     let
       val thy = theory_of_thm thm;
@@ -1013,13 +1013,14 @@
 
       val ps = map (apsnd (Future.map fulfill_body)) promises;
       val (pthm, proof) =
-        Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy) name shyps hyps prop ps body;
+        Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy)
+          name_pos shyps hyps prop ps body;
       val der' = make_deriv [] [] [pthm] proof;
     in Thm (der', args) end);
 
-val close_derivation =
+fun close_derivation pos =
   solve_constraints #> (fn thm =>
-    if derivation_closed thm then thm else name_derivation "" thm);
+    if derivation_closed thm then thm else name_derivation ("", pos) thm);
 
 val trim_context = solve_constraints #> trim_context_thm;
 
@@ -1688,7 +1689,8 @@
 
       val ps = map (apsnd (Future.map fulfill_body)) promises;
       val (pthm, proof) =
-        Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy) shyps prop ps body;
+        Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy)
+          shyps prop ps body;
       val der' = make_deriv [] [] [pthm] proof;
       val prop' = Proofterm.thm_node_prop (#2 pthm);
     in
@@ -2207,7 +2209,7 @@
               |> (map_classrels o Symreltab.update) ((c1, c2),
                 (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
                 |> standard_tvars
-                |> close_derivation
+                |> close_derivation \<^here>
                 |> trim_context));
 
         val proven = is_classrel thy1;
@@ -2240,7 +2242,7 @@
             val th1 =
               (th RS the_classrel thy (c, c1))
               |> standard_tvars
-              |> close_derivation
+              |> close_derivation \<^here>
               |> trim_context;
           in SOME ((t, Ss, c1), (th1, thy_name, ser)) end);
     val finished' = finished andalso null completions;