src/HOL/Tools/BNF/bnf_lfp.ML

     val b_names = map Binding.name_of bs;
     val b_name = mk_common_name b_names;
     val b = Binding.name b_name;
 
     fun mk_internal_of_b name =
-      Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.conceal;
+      Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.concealed;
     fun mk_internal_b name = mk_internal_of_b name b;
     fun mk_internal_bs name = map (mk_internal_of_b name) bs;
     val external_bs = map2 (Binding.prefix false) b_names bs
-      |> not note_all ? map Binding.conceal;
+      |> not note_all ? map Binding.concealed;
 
     val deads = fold (union (op =)) Dss resDs;
     val names_lthy = fold Variable.declare_typ deads lthy;
     val passives = map fst (subtract (op = o apsnd TFree) deads resBs);
 

     val Izs = map2 retype_const_or_free Ts zs;
     val phis = map2 retype_const_or_free (map mk_pred1T Ts) init_phis;
     val phi2s = map2 retype_const_or_free (map2 mk_pred2T Ts Ts') init_phis;
 
     fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
-    val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
+    val ctor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o ctor_bind;
 
     fun ctor_spec abs str map_FT_init =
       Library.foldl1 HOLogic.mk_comp [abs, str,
         Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts)];
 

     val fold_fun = Term.absfree fold_f'
       (mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n fold_f) ks));
     val foldx = HOLogic.choice_const foldT $ fold_fun;
 
     fun fold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_foldN ^ "_");
-    val fold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o fold_bind;
+    val fold_def_bind = rpair [] o Binding.concealed o Thm.def_binding o fold_bind;
 
     fun fold_spec i = fold_rev (Term.absfree o Term.dest_Free) ss (mk_nthN n foldx i);
 
     val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) =
       lthy

     val map_ctors = map2 (fn Ds => fn bnf =>
       Term.list_comb (mk_map_of_bnf Ds (passiveAs @ FTs) (passiveAs @ Ts) bnf,
         map HOLogic.id_const passiveAs @ ctors)) Dss bnfs;
 
     fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
-    val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind;
+    val dtor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o dtor_bind;
 
     fun dtor_spec i = mk_fold Ts map_ctors i;
 
     val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
       lthy

         map2 (fn unique => fn fold_ctor =>
           trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms
       end;
 
     fun rec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_recN ^ "_");
-    val rec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o rec_bind;
+    val rec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o rec_bind;
 
     val rec_strs =
       @{map 3} (fn ctor => fn prod_s => fn mapx =>
         mk_convol (HOLogic.mk_comp (ctor, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s))
       ctors rec_ss rec_maps;