equal
deleted
inserted
replaced
59 structure Nominal_Library: NOMINAL_LIBRARY = |
59 structure Nominal_Library: NOMINAL_LIBRARY = |
60 struct |
60 struct |
61 |
61 |
62 fun last2 [] = raise Empty |
62 fun last2 [] = raise Empty |
63 | last2 [_] = raise Empty |
63 | last2 [_] = raise Empty |
64 | last2 [x, y] = (x,y) |
64 | last2 [x, y] = (x, y) |
65 | last2 (_ :: xs) = last2 xs |
65 | last2 (_ :: xs) = last2 xs |
66 |
66 |
67 fun dest_listT (Type (@{type_name list}, [T])) = T |
67 fun dest_listT (Type (@{type_name list}, [T])) = T |
68 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
68 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
69 |
69 |