equal
deleted
inserted
replaced
1 structure ROOT = |
1 structure ROOT = |
2 struct |
2 struct |
3 |
3 |
4 structure Code_Generator = |
4 structure HOL = |
5 struct |
5 struct |
6 |
6 |
7 type 'a eq = {eq : 'a -> 'a -> bool}; |
7 type 'a eq = {eq : 'a -> 'a -> bool}; |
8 fun eq (A_:'a eq) = #eq A_; |
8 fun eq (A_:'a eq) = #eq A_; |
9 |
9 |
10 end; (*struct Code_Generator*) |
10 end; (*struct HOL*) |
11 |
11 |
12 structure List = |
12 structure List = |
13 struct |
13 struct |
14 |
14 |
15 fun memberl A_ x (y :: ys) = |
15 fun memberl A_ x (y :: ys) = HOL.eq A_ x y orelse memberl A_ x ys |
16 Code_Generator.eq A_ x y orelse memberl A_ x ys |
|
17 | memberl A_ x [] = false; |
16 | memberl A_ x [] = false; |
18 |
17 |
19 end; (*struct List*) |
18 end; (*struct List*) |
20 |
19 |
21 structure Codegen = |
20 structure Codegen = |