equal
deleted
inserted
replaced
278 |
278 |
279 (* alignment *) |
279 (* alignment *) |
280 |
280 |
281 fun align_left msg xs ys = |
281 fun align_left msg xs ys = |
282 let val m = length xs and n = length ys |
282 let val m = length xs and n = length ys |
283 in if m < n then error msg else ((uncurry take) (n, xs) ~~ ys) end; |
283 in if m < n then error msg else (take n xs ~~ ys) end; |
284 |
284 |
285 fun align_right msg xs ys = |
285 fun align_right msg xs ys = |
286 let val m = length xs and n = length ys |
286 let val m = length xs and n = length ys |
287 in if m < n then error msg else ((uncurry drop) (m - n, xs) ~~ ys) end; |
287 in if m < n then error msg else (drop (m - n) xs ~~ ys) end; |
288 |
288 |
289 |
289 |
290 (* prep_inst *) |
290 (* prep_inst *) |
291 |
291 |
292 fun prep_inst ctxt align tune (tm, ts) = |
292 fun prep_inst ctxt align tune (tm, ts) = |