src/HOL/Tools/Datatype/datatype_data.ML

   (info_of_case (ProofContext.theory_of ctxt));
 
 fun add_case_tr' case_names thy =
   Sign.add_advanced_trfuns ([], [],
     map (fn case_name =>
-      let val case_name' = Syntax.mark_const case_name
+      let val case_name' = Lexicon.mark_const case_name
       in (case_name', Datatype_Case.case_tr' info_of_case case_name')
       end) case_names, []) thy;
 
 val trfun_setup =
   Sign.add_advanced_trfuns ([],