| changeset 41491 | a2ad5b824051 |
| parent 41490 | 0f1e411a1448 |
| child 41521 | c704c437ec74 |
| 41490:0f1e411a1448 | 41491:a2ad5b824051 |
|---|---|
463 in |
463 in |
464 (t' $ u',idx'') |
464 (t' $ u',idx'') |
465 end |
465 end |
466 | F (Abs(x,xT,t),idx) = |
466 | F (Abs(x,xT,t),idx) = |
467 let |
467 let |
468 val x' = "x" ^ Int.toString idx |
468 val x' = "x" ^ string_of_int idx |
469 val (t',idx') = F (t,idx+1) |
469 val (t',idx') = F (t,idx+1) |
470 in |
470 in |
471 (Abs(x',xT,t'),idx') |
471 (Abs(x',xT,t'),idx') |
472 end |
472 end |
473 | F arg = arg |
473 | F arg = arg |