145 (* specifications *) |
145 (* specifications *) |
146 |
146 |
147 fun disjoint_specs context c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) = |
147 fun disjoint_specs context c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) = |
148 Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) => |
148 Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) => |
149 i = j orelse disjoint_args (Ts, Us) orelse |
149 i = j orelse disjoint_args (Ts, Us) orelse |
150 error ("Clash of specifications for " ^ Pretty.str_of (pretty_item context c) ^ ":\n" ^ |
150 error ("Clash of specifications for " ^ |
|
151 Pretty.unformatted_string_of (pretty_item context c) ^ ":\n" ^ |
151 " " ^ quote a ^ Position.here pos_a ^ "\n" ^ |
152 " " ^ quote a ^ Position.here pos_a ^ "\n" ^ |
152 " " ^ quote b ^ Position.here pos_b)); |
153 " " ^ quote b ^ Position.here pos_b)); |
153 |
154 |
154 fun join_specs context c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) = |
155 fun join_specs context c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) = |
155 let |
156 let |