equal
deleted
inserted
replaced
83 |
83 |
84 (* Parameters of expression (not expression_i). |
84 (* Parameters of expression (not expression_i). |
85 Sanity check of instantiations. |
85 Sanity check of instantiations. |
86 Positional instantiations are extended to match full length of parameter list. *) |
86 Positional instantiations are extended to match full length of parameter list. *) |
87 |
87 |
88 fun parameters thy (expr, fixed) = |
88 fun parameters thy (expr, fixed : (Name.binding * string option * mixfix) list) = |
89 let |
89 let |
90 fun reject_dups message xs = |
90 fun reject_dups message xs = |
91 let val dups = duplicates (op =) xs |
91 let val dups = duplicates (op =) xs |
92 in |
92 in |
93 if null dups then () else error (message ^ commas dups) |
93 if null dups then () else error (message ^ commas dups) |