equal
deleted
inserted
replaced
55 | Abs (x, T, t) => Abs (x, typ T, term t) |
55 | Abs (x, T, t) => Abs (x, typ T, term t) |
56 | t $ u => term t $ term u); |
56 | t $ u => term t $ term u); |
57 val _ = Unsynchronized.change terms (Syntax_Termtab.update (tm', ())); |
57 val _ = Unsynchronized.change terms (Syntax_Termtab.update (tm', ())); |
58 in tm' end); |
58 in tm' end); |
59 |
59 |
60 in (typ, term) end; |
60 fun check eq f x = |
|
61 let val x' = f x in |
|
62 if eq (x, x') then x' |
|
63 else raise Fail "Something is utterly wrong" |
|
64 end; |
|
65 |
|
66 in (check (op =) typ, check (op =) term) end; |
61 |
67 |
62 val typs = map o #1 o init; |
68 val typs = map o #1 o init; |
63 val terms = map o #2 o init; |
69 val terms = map o #2 o init; |
64 |
70 |
65 end; |
71 end; |