src/Pure/tactic.ML
changeset 761 04320c295500
parent 670 ff4c6691de9d
child 922 196ca0973a6d
equal deleted inserted replaced
760:f0200e91b272 761:04320c295500
   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 =