133 NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env |
133 NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env |
134 | SOME Ts => (Ts, env)); |
134 | SOME Ts => (Ts, env)); |
135 val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts) |
135 val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts) |
136 (Proofterm.forall_intr_vfs prop) handle ListPair.UnequalLengths => |
136 (Proofterm.forall_intr_vfs prop) handle ListPair.UnequalLengths => |
137 error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf)) |
137 error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf)) |
138 in (prop', Proofterm.change_type (SOME Ts) prf, [], env', vTs) end; |
138 in (prop', Proofterm.change_types (SOME Ts) prf, [], env', vTs) end; |
139 |
139 |
140 fun head_norm (prop, prf, cnstrts, env, vTs) = |
140 fun head_norm (prop, prf, cnstrts, env, vTs) = |
141 (Envir.head_norm env prop, prf, cnstrts, env, vTs); |
141 (Envir.head_norm env prop, prf, cnstrts, env, vTs); |
142 |
142 |
143 fun mk_cnstrts env _ Hs vTs (PBound i) = ((nth Hs i, PBound i, [], env, vTs) |
143 fun mk_cnstrts env _ Hs vTs (PBound i) = ((nth Hs i, PBound i, [], env, vTs) |