equal
deleted
inserted
replaced
83 fun plain_args args = |
83 fun plain_args args = |
84 forall Term.is_TVar args andalso not (has_duplicates (op =) args); |
84 forall Term.is_TVar args andalso not (has_duplicates (op =) args); |
85 |
85 |
86 fun disjoint_args (Ts, Us) = |
86 fun disjoint_args (Ts, Us) = |
87 not (Type.could_unifys (Ts, Us)) orelse |
87 not (Type.could_unifys (Ts, Us)) orelse |
88 ((Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us) Vartab.empty; false) |
88 ((Vartab.build (Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us)); false) |
89 handle Type.TUNIFY => true); |
89 handle Type.TUNIFY => true); |
90 |
90 |
91 fun match_args (Ts, Us) = |
91 fun match_args (Ts, Us) = |
92 if Type.could_matches (Ts, Us) then |
92 if Type.could_matches (Ts, Us) then |
93 Option.map Envir.subst_type |
93 Option.map Envir.subst_type |
94 (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE) |
94 (SOME (Vartab.build (Type.raw_matches (Ts, Us))) handle Type.TYPE_MATCH => NONE) |
95 else NONE; |
95 else NONE; |
96 |
96 |
97 |
97 |
98 (* datatype defs *) |
98 (* datatype defs *) |
99 |
99 |