src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

 
         val cxIns = map2 (mk_cIn ctor) ks xss;
         val cyIns = map2 (mk_cIn (Term.map_types B_ify_T ctor)) ks yss;
 
         fun mk_map_thm ctr_def' cxIn =
-          fold_thms lthy [ctr_def']
+          Local_Defs.fold lthy [ctr_def']
             (unfold_thms lthy (o_apply :: pre_map_def ::
                  (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_map @ abs_inverses)
                (infer_instantiate' lthy (map (SOME o Thm.cterm_of lthy) fs @ [SOME cxIn])
                   (if fp = Least_FP then fp_map_thm
                    else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans))))
           |> singleton (Proof_Context.export names_lthy lthy);
 
         fun mk_set0_thm fp_set_thm ctr_def' cxIn =
-          fold_thms lthy [ctr_def']
+          Local_Defs.fold lthy [ctr_def']
             (unfold_thms lthy (pre_set_defs @ fp_nesting_set_maps @ live_nesting_set_maps @
                  (if fp = Least_FP then [] else [dtor_ctor]) @ basic_sumprod_thms_set @
                  @{thms UN_Un sup_assoc[THEN sym]} @ abs_inverses)
                (infer_instantiate' lthy [SOME cxIn] fp_set_thm))
           |> singleton (Proof_Context.export names_lthy lthy);

           |> map (unfold_thms lthy @{thms insert_is_Un[THEN sym] Un_empty_left Un_insert_left});
 
         val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
 
         fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
-          fold_thms lthy ctr_defs'
+          Local_Defs.fold lthy ctr_defs'
             (unfold_thms lthy (pre_rel_def :: abs_inverses @
                  (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
                  @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]})
                (infer_instantiate' lthy (map (SOME o Thm.cterm_of lthy) Rs @ [SOME cxIn, SOME cyIn])
                   fp_rel_thm))