equal
deleted
inserted
replaced
623 (* convert n-tuple to nested pairs *) |
623 (* convert n-tuple to nested pairs *) |
624 |
624 |
625 fun conv_ntuple fs ts p = |
625 fun conv_ntuple fs ts p = |
626 let |
626 let |
627 val k = length fs; |
627 val k = length fs; |
628 val xs = map (fn i => str ("x" ^ string_of_int i)) (0 upto k); |
628 val xs = map_range (fn i => str ("x" ^ string_of_int i)) (k + 1); |
629 val xs' = map (fn Bound i => nth xs (k - i)) ts; |
629 val xs' = map (fn Bound i => nth xs (k - i)) ts; |
630 fun conv xs js = |
630 fun conv xs js = |
631 if js mem fs then |
631 if js mem fs then |
632 let |
632 let |
633 val (p, xs') = conv xs (1::js); |
633 val (p, xs') = conv xs (1::js); |