src/HOL/Tools/Old_Datatype/old_primrec.ML

       if Binding.name_of b = fname then SOME ((b, mx), T) else NONE) fixes;
     val def_name = Thm.def_name (Long_Name.base_name fname);
     val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t)) (map snd ls @ [dummyT])
       (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
     val rhs = singleton (Syntax.check_terms ctxt) (Type.constraint varT raw_rhs);
-  in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end;
+  in (var, ((Binding.concealed (Binding.name def_name), []), rhs)) end;
 
 
 (* find datatypes which contain all datatypes in tnames' *)
 
 fun find_dts _ _ [] = []