src/HOL/Tools/Datatype/datatype.ML
changeset 36148 4ddcc2b07891
parent 35994 9cc3df9a606e
child 36692 54b64d4ad524
equal deleted inserted replaced
36147:b43b22f63665 36148:4ddcc2b07891
   680             val c = Sign.full_name_path tmp_thy tname' cname;
   680             val c = Sign.full_name_path tmp_thy tname' cname;
   681           in
   681           in
   682             (constrs @ [(c, map (dtyp_of_typ new_dts) cargs')],
   682             (constrs @ [(c, map (dtyp_of_typ new_dts) cargs')],
   683               constr_syntax' @ [(cname, mx')], sorts'')
   683               constr_syntax' @ [(cname, mx')], sorts'')
   684           end handle ERROR msg => cat_error msg
   684           end handle ERROR msg => cat_error msg
   685            ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
   685            ("The error above occurred in constructor " ^ quote (Binding.str_of cname) ^
   686             " of datatype " ^ quote (Binding.str_of tname));
   686             " of datatype " ^ quote (Binding.str_of tname));
   687 
   687 
   688         val (constrs', constr_syntax', sorts') =
   688         val (constrs', constr_syntax', sorts') =
   689           fold prep_constr constrs ([], [], sorts)
   689           fold prep_constr constrs ([], [], sorts)
   690       in
   690       in