src/HOL/Tools/BNF/bnf_fp_util.ML

 
     fun flatten_tyargs Ass =
       subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs;
 
     fun raw_qualify base_b =
-      let val (_, qs, n) = Binding.dest base_b;
+      let
+        val qs = Binding.path_of base_b;
+        val n = Binding.name_of base_b;
       in
         Binding.prefix_name rawN
         #> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)])
-        #> Binding.conceal
+        #> Binding.concealed
       end;
 
     val ((bnfs, (deadss, livess)), accum) =
       apfst (apsnd split_list o split_list)
         (@{fold_map 2}
           (fn b => bnf_of_typ Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs
           ((empty_comp_cache, empty_unfolds), lthy));
 
     fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))))
-      #> Binding.conceal;
+      #> Binding.concealed;
 
     val Ass = map (map dest_TFree) livess;
     val Ds' = fold (fold Term.add_tfreesT) deadss [];
     val Ds = union (op =) Ds' Ds0;
     val missing = resBs |> fold (subtract (op =)) (Ds' :: Ass);

       normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs accum;
 
     val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss;
 
     fun pre_qualify b = Binding.qualify false (Binding.name_of b)
-      #> not (Config.get lthy' bnf_note_all) ? Binding.conceal;
+      #> not (Config.get lthy' bnf_note_all) ? Binding.concealed;
 
     val ((pre_bnfs, (deadss, absT_infos)), lthy'') =
       @{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
         bs (not (null live_phantoms) :: replicate (nn - 1) false) Dss bnfs' lthy'
       |>> split_list