src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

     timer; lthy'
   end;
 
 val datatypes = define_datatypes (K I) (K I) (K I);
 
-val datatype_cmd = define_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.read_term;
+val datatype_cmd = define_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term;
 
 val parse_ctr_arg =
   @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
   (Parse.typ >> pair Binding.empty);