1085 val subst = TermSubst.instantiate_maxidx (instT', inst'); |
1085 val subst = TermSubst.instantiate_maxidx (instT', inst'); |
1086 val (prop', maxidx1) = subst prop ~1; |
1086 val (prop', maxidx1) = subst prop ~1; |
1087 val (tpairs', maxidx') = |
1087 val (tpairs', maxidx') = |
1088 fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1; |
1088 fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1; |
1089 in |
1089 in |
1090 if has_duplicates (fn ((v, _), (v', _)) => Term.eq_var (v, v')) inst' then |
1090 Thm {thy_ref = thy_ref', |
1091 raise THM ("instantiate: variables not distinct", 0, [th]) |
1091 der = Pt.infer_derivs' (fn d => |
1092 else if has_duplicates (fn ((v, _), (v', _)) => Term.eq_tvar (v, v')) instT' then |
1092 Pt.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der, |
1093 raise THM ("instantiate: type variables not distinct", 0, [th]) |
1093 maxidx = maxidx', |
1094 else |
1094 shyps = shyps', |
1095 Thm {thy_ref = thy_ref', |
1095 hyps = hyps, |
1096 der = Pt.infer_derivs' (fn d => |
1096 tpairs = tpairs', |
1097 Pt.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der, |
1097 prop = prop'} |
1098 maxidx = maxidx', |
|
1099 shyps = shyps', |
|
1100 hyps = hyps, |
|
1101 tpairs = tpairs', |
|
1102 prop = prop'} |
|
1103 end |
1098 end |
1104 handle TYPE (msg, _, _) => raise THM (msg, 0, [th]); |
1099 handle TYPE (msg, _, _) => raise THM (msg, 0, [th]); |
1105 |
1100 |
1106 end; |
1101 end; |
1107 |
1102 |