src/HOL/HOLCF/Tools/Domain/domain_constructors.ML

     end
 
     (* define syntax for case combinator *)
     (* TODO: re-implement case syntax using a parse translation *)
     local
-      fun syntax c = Syntax.mark_const (fst (dest_Const c))
+      fun syntax c = Lexicon.mark_const (fst (dest_Const c))
       fun xconst c = Long_Name.base_name (fst (dest_Const c))
       fun c_ast authentic con = Ast.Constant (if authentic then syntax con else xconst con)
       fun showint n = string_of_int (n+1)
       fun expvar n = Ast.Variable ("e" ^ showint n)
       fun argvar n (m, _) = Ast.Variable ("a" ^ showint n ^ "_" ^ showint m)