src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML

 
     val dtor_ctor = nth dtor_ctors fp_res_index;
   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 =
   let
     val SOME {casex, exhaust, case_thms, ...} = ctr_sugar_of ctxt fpT_name;

     val exhaust' = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt var)] exhaust;
   in
     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 =
   [mk_abs_transfer ctxt fpT_name, mk_rep_transfer ctxt fpT_name]
   handle Fail _ => [];

       mk_code_tac ctxt num_args fpsig_nesting_maps ssig_map eval pre_map_def abs_inverse
         fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms
         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
     {sig_fp_sugars, ssig_fp_sugar, eval, eval_simps, all_algLam_algs, corecUU_unique, ...} fpT_name
     eq_corecUU =

       mk_unique_tac ctxt num_args fpsig_nesting_maps ssig_map eval pre_map_def abs_inverse
         fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms
         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 =
   let
     val SOME {T = fcT, discs, exhaust, disc_thmss, ...} = ctr_sugar_of ctxt fcT_name;

 
     val goal = mk_Trueprop_eq (last_udisc, foldr1 HOLogic.mk_conj not_udiscs);
   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,
       corecUU_unique, ...}
     ({algrho = algrho0, dtor_algrho, ...} : friend_info) fun_t k_T code_goal const_transfers rho_def

           fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms
           live_nesting_map_ident0s fp_map_ident dtor_ctor ctor_iff_dtor ctr_defs nullary_disc_defs
           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
         | thm_nones =>
           error ("Failed to state naturality property for " ^

 
     fun derive_unprimed rho_transfer' =
       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
     if null abs_rep_transfers then (goal', derive_unprimed #> fold_rho)
     else (goal, fold_rho)

     Variable.add_free_names ctxt goal []
     |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
       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 =
   let
     val xy_Ts = binder_types (fastype_of alg);

 
     fun prove ctr_def goal =
       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
     map2 prove ctr_defs goals
   end;

     val goal = mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong friend;
   in
     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
     ({cong_base, cong_refl, cong_sym, cong_trans, cong_alg_intros, ...} : dtor_coinduct_info) =
   let

       mk_eq_corecUU_tac ctxt num_args fpsig_nesting_maps ssig_map eval pre_map_def abs_inverse
         fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms
         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
     ({fpT = fpT0 as Type (fpT_name, _), friend_names = friend_names0,
       corecUU = Const (corecUU_name, _), dtor_coinduct_info as {dtor_coinduct, ...}, ...})

 
     fun prove_transfer_goal ctxt goal =
       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
         SOME thm => apfst (cons thm)
       | NONE => apsnd (cons goal));