src/HOL/Tools/BNF/bnf_comp.ML

         val goal = mk_Trueprop_eq (var_set', set);
         fun tac {context = ctxt, prems = _} =
           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)
       end;
 

           val bd_bd' = HOLogic.mk_prod (bd, bd');
           val ordIso = Const (\<^const_name>\<open>ordIso\<close>, HOLogic.mk_setT (fastype_of bd_bd'));
           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);
 
     fun map_id0_tac ctxt =

       else
         map (fn goal =>
           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 =
       mk_comp_map_cong0_tac ctxt set'_eq_sets set_alt_thms (map_cong0_of_bnf outer)
         (map map_cong0_of_bnf inners);

         val in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA;
         val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
       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)
       (map le_rel_OO_of_bnf inners);
 

         val inx = mk_in Asets sets T;
         val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T;
         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 =
       EVERY' [rtac ctxt @{thm ord_le_eq_trans}, rtac ctxt (le_rel_OO_of_bnf bnf)] 1 THEN
       unfold_thms_tac ctxt @{thms eq_OO} THEN rtac ctxt refl 1;

         val inx = mk_in Asets sets T;
         val in_alt = mk_in (drop n Asets) bnf_sets T;
         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;
 
     fun rel_OO_Grp_tac ctxt = mk_simple_rel_OO_Grp_tac ctxt (rel_OO_Grp_of_bnf bnf) in_alt_thm;

         val in_alt = mk_in (unpermute Asets) bnf_sets T;
         val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt));
       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;
 
     fun rel_OO_Grp_tac ctxt = mk_simple_rel_OO_Grp_tac ctxt (rel_OO_Grp_of_bnf bnf) in_alt_thm;