src/HOL/Tools/inductive.ML

         Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
       else alt_name;
 
     val is_auxiliary = length cs >= 2; 
     val ((rec_const, (_, fp_def)), lthy') = lthy
-      |> is_auxiliary ? Local_Theory.conceal
+      |> is_auxiliary ? Local_Theory.concealed
       |> Local_Theory.define
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
-         ((Binding.conceal (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}),
+         ((Binding.concealed (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}),
            fold_rev lambda params
              (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
       ||> is_auxiliary ? Local_Theory.restore_naming lthy;
     val fp_def' =
       Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])

           let
             val Ts = arg_types_of (length params) c;
             val xs =
               map Free (Variable.variant_frees lthy intr_ts (mk_names "x" (length Ts) ~~ Ts));
           in
-            (name_mx, (apfst Binding.conceal Attrib.empty_binding, fold_rev lambda (params @ xs)
+            (name_mx, (apfst Binding.concealed Attrib.empty_binding, fold_rev lambda (params @ xs)
               (list_comb (rec_const, params @ make_bool_args' bs i @
                 make_args argTs (xs ~~ Ts)))))
           end) (cnames_syn ~~ cs);
     val (consts_defs, lthy'') = lthy'
       |> fold_map Local_Theory.define specs;
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
     val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
     val mono = prove_mono quiet_mode skip_mono predT fp_fun monos lthy''';
     val (_, lthy'''') =
-      Local_Theory.note (apfst Binding.conceal Attrib.empty_binding,
+      Local_Theory.note (apfst Binding.concealed Attrib.empty_binding,
         Proof_Context.export lthy''' lthy'' [mono]) lthy'';
 
   in (lthy'''', lthy''', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
     list_comb (rec_const, params), preds, argTs, bs, xs)
   end;