equal
deleted
inserted
replaced
394 |
394 |
395 (*order-sorted unification*) |
395 (*order-sorted unification*) |
396 fun unify (tsig as TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) = |
396 fun unify (tsig as TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) = |
397 let |
397 let |
398 val tyvar_count = ref maxidx; |
398 val tyvar_count = ref maxidx; |
399 fun gen_tyvar S = TVar (("'a", inc tyvar_count), S); |
399 fun gen_tyvar S = TVar ((Name.aT, inc tyvar_count), S); |
400 |
400 |
401 fun mg_domain a S = Sorts.mg_domain classes a S |
401 fun mg_domain a S = Sorts.mg_domain classes a S |
402 handle Sorts.CLASS_ERROR _ => raise TUNIFY; |
402 handle Sorts.CLASS_ERROR _ => raise TUNIFY; |
403 |
403 |
404 fun meet (_, []) tye = tye |
404 fun meet (_, []) tye = tye |