equal
deleted
inserted
replaced
1760 fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy = |
1760 fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy = |
1761 let |
1761 let |
1762 val external_names = NameSpace.external_names (Sign.naming_of thy); |
1762 val external_names = NameSpace.external_names (Sign.naming_of thy); |
1763 |
1763 |
1764 val alphas = map fst args; |
1764 val alphas = map fst args; |
1765 val name = Sign.full_name thy bname; |
1765 val name = Sign.full_bname thy bname; |
1766 val full = Sign.full_name_path thy bname; |
1766 val full = Sign.full_bname_path thy bname; |
1767 val base = Sign.base_name; |
1767 val base = Sign.base_name; |
1768 |
1768 |
1769 val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields); |
1769 val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields); |
1770 |
1770 |
1771 val parent_fields = List.concat (map #fields parents); |
1771 val parent_fields = List.concat (map #fields parents); |
2251 val args = map (fn x => (x, AList.lookup (op =) envir x |> the_default defaultS)) params; |
2251 val args = map (fn x => (x, AList.lookup (op =) envir x |> the_default defaultS)) params; |
2252 |
2252 |
2253 |
2253 |
2254 (* errors *) |
2254 (* errors *) |
2255 |
2255 |
2256 val name = Sign.full_name thy bname; |
2256 val name = Sign.full_bname thy bname; |
2257 val err_dup_record = |
2257 val err_dup_record = |
2258 if is_none (get_record thy name) then [] |
2258 if is_none (get_record thy name) then [] |
2259 else ["Duplicate definition of record " ^ quote name]; |
2259 else ["Duplicate definition of record " ^ quote name]; |
2260 |
2260 |
2261 val err_dup_parms = |
2261 val err_dup_parms = |