--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Mar 08 13:21:58 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Mar 08 14:15:39 2013 +0100
@@ -1165,7 +1165,7 @@
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 ")"} ||