src/HOL/Tools/BNF/bnf_lfp.ML

             |> singleton (Proof_Context.export names_lthy lthy))
           (map mk_mono_goal min_algss) min_algs_thms;
 
         fun mk_card_conjunct min_alg = mk_ordLeq (mk_card_of min_alg) Asuc_bd;
         val card_conjunction = Library.foldr1 HOLogic.mk_conj (map mk_card_conjunct min_algss);
-        val card_cT = certifyT lthy suc_bdT;
-        val card_ct = certify lthy (Term.absfree idx' card_conjunction);
+        val card_cT = Proof_Context.ctyp_of lthy suc_bdT;
+        val card_ct = Proof_Context.cterm_of lthy (Term.absfree idx' card_conjunction);
 
         val card_of =
           Goal.prove_sorry lthy [] []
             (HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, card_conjunction)))
             (K (mk_min_algs_card_of_tac card_cT card_ct

           |> Thm.close_derivation
           |> singleton (Proof_Context.export names_lthy lthy);
 
         val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_leq min_algss Bs);
-        val least_cT = certifyT lthy suc_bdT;
-        val least_ct = certify lthy (Term.absfree idx' least_conjunction);
+        val least_cT = Proof_Context.ctyp_of lthy suc_bdT;
+        val least_ct = Proof_Context.cterm_of lthy (Term.absfree idx' least_conjunction);
 
         val least =
           (Goal.prove_sorry lthy [] []
             (Logic.mk_implies (least_prem,
               HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, least_conjunction))))

     val str_init_defs = map (fn def =>
       mk_unabs_def 2 (Morphism.thm phi def RS meta_eq_to_obj_eq)) str_init_def_frees;
 
     val car_inits = map (mk_min_alg str_inits) ks;
 
-    val alg_init_thm = cterm_instantiate_pos (map (SOME o certify lthy) str_inits) alg_min_alg_thm;
+    val alg_init_thm = cterm_instantiate_pos (map (SOME o Proof_Context.cterm_of lthy) str_inits) alg_min_alg_thm;
 
     val alg_select_thm = Goal.prove_sorry lthy [] []
       (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)

           [mk_mor car_inits str_inits Bs ss init_fs,
           mk_mor car_inits str_inits Bs ss init_fs_copy];
         fun mk_fun_eq f g x = HOLogic.mk_eq (f $ x, g $ x);
         val unique = HOLogic.mk_Trueprop
           (Library.foldr1 HOLogic.mk_conj (@{map 3} mk_fun_eq init_fs init_fs_copy init_xs));
-        val cts = map (certify lthy) ss;
+        val cts = map (Proof_Context.cterm_of lthy) ss;
         val unique_mor =
           Goal.prove_sorry lthy [] [] (Logic.list_implies (prems @ mor_prems, unique))
             (K (mk_init_unique_mor_tac cts m alg_def alg_init_thm least_min_alg_thms
               in_mono'_thms alg_set_thms morE_thms map_cong0s))
           |> Thm.close_derivation

             (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;
 
         fun mk_ct initFT str abs = Term.absdummy initFT (abs $ (str $ Bound 0))
-        val cts = @{map 3} (certify lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
+        val cts = @{map 3} (Proof_Context.cterm_of lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
 
         val mor_Abs =
           Goal.prove_sorry lthy [] []
             (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

       end;
 
     val mor_fold_thm =
       let
         val mor_cong = mor_cong_thm OF (map (mk_nth_conv n) ks);
-        val cT = certifyT lthy foldT;
-        val ct = certify lthy fold_fun
+        val cT = Proof_Context.ctyp_of lthy foldT;
+        val ct = Proof_Context.cterm_of lthy fold_fun
       in
         Goal.prove_sorry lthy [] []
           (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks)))
           (fn {context = ctxt, ...} =>
             mk_mor_fold_tac ctxt cT ct fold_defs init_ex_mor_thm mor_cong)

         |> Thm.close_derivation
         |> singleton (Proof_Context.export names_lthy lthy),
         rev (Term.add_tfrees goal []))
       end;
 
-    val cTs = map (SOME o certifyT lthy o TFree) induct_params;
+    val cTs = map (SOME o Proof_Context.ctyp_of lthy o TFree) induct_params;
 
     val weak_ctor_induct_thms =
       let fun insts i = (replicate (i - 1) TrueI) @ (asm_rl :: replicate (n - i) TrueI);
       in map (fn i => (ctor_induct_thm OF insts i) RS mk_conjunctN n i) ks end;
 

         fun mk_concl phi z1 z2 = phi $ z1 $ z2;
         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
           (@{map 3} mk_concl phi2s Izs1 Izs2));
         fun mk_t phi (z1, z1') (z2, z2') =
           Term.absfree z1' (HOLogic.mk_all (fst z2', snd z2', phi $ z1 $ z2));
-        val cts = @{map 3} (SOME o certify lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2');
+        val cts = @{map 3} (SOME o Proof_Context.cterm_of lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2');
         val goal = Logic.list_implies (prems, concl);
       in
         (Goal.prove_sorry lthy [] [] goal
           (fn {context = ctxt, prems = _} => mk_ctor_induct2_tac ctxt cTs cts ctor_induct_thm
             weak_ctor_induct_thms)

             (1 upto n);
         val set_Iset_thmsss = transpose (map (map mk_set_thms) ctor_Iset_thmss);
 
         val timer = time (timer "set functions for the new datatypes");
 
-        val cxs = map (SOME o certify lthy) Izs;
+        val cxs = map (SOME o Proof_Context.cterm_of lthy) Izs;
         val Isetss_by_range' =
           map (map (Term.subst_atomic_types (passiveAs ~~ passiveBs))) Isetss_by_range;
 
         val Iset_Imap0_thmss =
           let
             fun mk_set_map0 f map z set set' =
               HOLogic.mk_eq (mk_image f $ (set $ z), set' $ (map $ z));
 
-            fun mk_cphi f map z set set' = certify lthy
+            fun mk_cphi f map z set set' = Proof_Context.cterm_of lthy
               (Term.absfree (dest_Free z) (mk_set_map0 f map z set set'));
 
-            val csetss = map (map (certify lthy)) Isetss_by_range';
+            val csetss = map (map (Proof_Context.cterm_of lthy)) Isetss_by_range';
 
             val cphiss = @{map 3} (fn f => fn sets => fn sets' =>
               (@{map 4} (mk_cphi f) fs_Imaps Izs sets sets')) fs Isetss_by_range Isetss_by_range';
 
             val inducts = map (fn cphis =>

 
         val Iset_bd_thmss =
           let
             fun mk_set_bd z bd set = mk_ordLeq (mk_card_of (set $ z)) bd;
 
-            fun mk_cphi z set = certify lthy (Term.absfree (dest_Free z) (mk_set_bd z sbd0 set));
+            fun mk_cphi z set = Proof_Context.cterm_of lthy (Term.absfree (dest_Free z) (mk_set_bd z sbd0 set));
 
             val cphiss = map (map2 mk_cphi Izs) Isetss_by_range;
 
             val inducts = map (fn cphis =>
               Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;

               HOLogic.mk_imp
                 (Library.foldr1 HOLogic.mk_conj (@{map 5} (mk_prem z) sets fs fs_copy ys ys'),
                 HOLogic.mk_eq (fmap $ z, gmap $ z));
 
             fun mk_cphi sets z fmap gmap =
-              certify lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap));
+              Proof_Context.cterm_of lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap));
 
             val cphis = @{map 4} mk_cphi Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps;
 
             val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm;
 

             fun mk_le_Irel_OO Irelpsi1 Irelpsi2 Irelpsi12 Iz1 Iz2 =
               HOLogic.mk_imp (mk_rel_compp (Irelpsi1, Irelpsi2) $ Iz1 $ Iz2,
                 Irelpsi12 $ Iz1 $ Iz2);
             val goals = @{map 5} mk_le_Irel_OO Irelpsi1s Irelpsi2s Irelpsi12s Izs1 Izs2;
 
-            val cTs = map (SOME o certifyT lthy o TFree) induct2_params;
-            val cxs = map (SOME o certify lthy) (splice Izs1 Izs2);
-            fun mk_cphi z1 z2 goal = SOME (certify lthy (Term.absfree z1 (Term.absfree z2 goal)));
+            val cTs = map (SOME o Proof_Context.ctyp_of lthy o TFree) induct2_params;
+            val cxs = map (SOME o Proof_Context.cterm_of lthy) (splice Izs1 Izs2);
+            fun mk_cphi z1 z2 goal = SOME (Proof_Context.cterm_of lthy (Term.absfree z1 (Term.absfree z2 goal)));
             val cphis = @{map 3} mk_cphi Izs1' Izs2' goals;
             val induct = Drule.instantiate' cTs (cphis @ cxs) ctor_induct2_thm;
 
             val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
           in