211 compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule), 
211 compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule), 
212 nsubgoal) i 
212 nsubgoal) i 
213 handle TERM (msg,_) => (writeln msg; no_tac) 
213 handle TERM (msg,_) => (writeln msg; no_tac) 
214  THM (msg,_,_) => (writeln msg; no_tac) ); 
214  THM (msg,_,_) => (writeln msg; no_tac) ); 
215 
215 
216 (*Resolve version*) 
216 (*"Resolve" version. Note: res_inst_tac cannot behave sensibly if the 

217 terms that are substituted contain (term or type) unknowns from the 

218 goal, because it is unable to instantiate goal unknowns at the same time. 

219 

220 The type checker freezes all flexible type vars that were introduced during 

221 type inference and still remain in the term at the end. This avoids the 

222 introduction of flexible type vars in goals and other places where they 

223 could cause complications. If you really want a flexible type var, you 

224 have to put it in yourself as a constraint. 

225 

226 This policy breaks down when a list of substitutions is type checked: later 

227 pairs may force type instantiations in earlier pairs, which is impossible, 

228 because the type vars in the earlier pairs are already frozen. 

229 *) 
217 fun res_inst_tac sinsts rule i = 
230 fun res_inst_tac sinsts rule i = 
218 compose_inst_tac sinsts (false, rule, nprems_of rule) i; 
231 compose_inst_tac sinsts (false, rule, nprems_of rule) i; 
219 
232 
220 (*eresolve (elimination) version*) 
233 (*eresolve (elimination) version*) 
221 fun eres_inst_tac sinsts rule i = 
234 fun eres_inst_tac sinsts rule i = 