equal
deleted
inserted
replaced
230 |
230 |
231 |
231 |
232 fun uni_constants (c1,ctp1) (c2,ctp2) = (c1 = c2) andalso (uni_types ctp1 ctp2); |
232 fun uni_constants (c1,ctp1) (c2,ctp2) = (c1 = c2) andalso (uni_types ctp1 ctp2); |
233 |
233 |
234 fun uni_mem _ [] = false |
234 fun uni_mem _ [] = false |
235 | uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) = (uni_constants (c,c_typ) (c1,c_typ1)) orelse (uni_mem (c,c_typ) ctyps); |
235 | uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) = (uni_constants (c1,c_typ1) (c,c_typ)) orelse (uni_mem (c,c_typ) ctyps); |
236 |
236 |
237 |
237 |
238 |
238 |
239 fun const_typ_of (Type (c,typs)) = CType (c,map const_typ_of typs) |
239 fun const_typ_of (Type (c,typs)) = CType (c,map const_typ_of typs) |
240 | const_typ_of (TFree(_,_)) = CTVar |
240 | const_typ_of (TFree(_,_)) = CTVar |