src/HOLCF/Tools/Domain/domain_syntax.ML

     val const_take   = (dbind "_take"  , HOLogic.natT-->dtype->>dtype, NoSyn);
     val const_finite = (dbind "_finite", dtype-->HOLogic.boolT       , NoSyn);
 
 (* ----- case translation --------------------------------------------------- *)
 
-    fun syntax b = Syntax.constN ^ Sign.full_bname thy b;
+    fun syntax b = Syntax.mark_const (Sign.full_bname thy b);
 
     local open Syntax in
     local
       fun c_ast authentic con = Constant ((authentic ? syntax) (Binding.name_of con));
       fun expvar n = Variable ("e" ^ string_of_int n);