src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML

   EVERY' [stac min_alg_def, rtac @{thm UN_least}, dtac least, dtac mp, atac,
     REPEAT_DETERM o etac conjE, atac] 1;
 
 fun mk_alg_select_tac Abs_inverse {context = ctxt, prems = _} =
   EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac] 1 THEN
-  Local_Defs.unfold_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
+  unfold_defs_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
 
 fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select
     alg_sets set_natural's str_init_defs =
   let
     val n = length alg_sets;

     REPEAT_DETERM o eresolve_tac [exE, conjE] THEN'
     REPEAT_DETERM o rtac exI THEN'
     rtac mor_select THEN' atac THEN' rtac CollectI THEN'
     REPEAT_DETERM o rtac exI THEN'
     rtac conjI THEN' rtac refl THEN' atac THEN'
-    K (Local_Defs.unfold_tac ctxt (Abs_inverse :: fst_snd_convs)) THEN'
+    K (unfold_defs_tac ctxt (Abs_inverse :: fst_snd_convs)) THEN'
     etac mor_comp THEN' etac mor_incl_min_alg) 1
   end;
 
 fun mk_init_unique_mor_tac m
     alg_def alg_min_alg least_min_algs in_monos alg_sets morEs map_congs =

   in
     CONJ_WRAP' mk_induct_tac least_min_algs 1
   end;
 
 fun mk_mor_Rep_tac fld_defs copy bijs inver_Abss inver_Reps {context = ctxt, prems = _} =
-  (K (Local_Defs.unfold_tac ctxt fld_defs) THEN' rtac conjunct1 THEN' rtac copy THEN'
+  (K (unfold_defs_tac ctxt fld_defs) THEN' rtac conjunct1 THEN' rtac copy THEN'
   EVERY' (map (fn bij => EVERY' [rtac bij, atac, etac bexI, rtac UNIV_I]) bijs) THEN'
   EVERY' (map rtac inver_Abss) THEN'
   EVERY' (map rtac inver_Reps)) 1;
 
 fun mk_mor_Abs_tac inv inver_Abss inver_Reps =

     EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply]))
       fld_o_iters),
     rtac sym, rtac id_apply] 1;
 
 fun mk_rec_tac rec_defs iter fst_recs {context = ctxt, prems = _}=
-  Local_Defs.unfold_tac ctxt
+  unfold_defs_tac ctxt
     (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN
   EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (iter RS @{thm arg_cong[of _ _ snd]}),
     rtac @{thm snd_convol'}] 1;
 
 fun mk_fld_induct_tac m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =

       EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
         rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
         CONJ_WRAP' (fn (set_simp, passive_set_natural) =>
           EVERY' [rtac ord_eq_le_trans, rtac set_simp, rtac @{thm Un_least},
             rtac ord_eq_le_trans, rtac @{thm box_equals[OF _ refl]},
-            rtac passive_set_natural, rtac trans_fun_cong_image_id_id_apply,
-            atac,
+            rtac passive_set_natural, rtac trans_fun_cong_image_id_id_apply, atac,
             CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
               (fn (active_set_natural, in_Irel) => EVERY' [rtac ord_eq_le_trans,
                 rtac @{thm UN_cong[OF _ refl]}, rtac active_set_natural, rtac @{thm UN_least},
                 dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
                 dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Irel RS iffD1),