| changeset 803 | 6f6ee78c7357 |
| parent 796 | 64f9c76f70c7 |
| child 807 | a5495a323b49 |
| 802:27a643e00675 | 803:6f6ee78c7357 |
|---|---|
66 (@{typ "('a * 'a) list"}, |
66 (@{typ "('a * 'a) list"}, |
67 @{typ "'a foo"}) |
67 @{typ "'a foo"}) |
68 *} |
68 *} |
69 |
69 |
70 ML {* |
70 ML {* |
71 test_funs repF @{context} |
|
72 (@{typ "(('a * 'a) list * 'b)"}, |
|
73 @{typ "('a foo * 'b)"}) |
|
74 *} |
|
75 |
|
76 ML {* |
|
71 test_funs absF @{context} |
77 test_funs absF @{context} |
72 (@{typ "(('a list) * int) list"}, |
78 (@{typ "(('a list) * int) list"}, |
73 @{typ "('a fset) bar"}) |
79 @{typ "('a fset) bar"}) |
74 *} |
80 *} |
75 |
81 |