[isabelle-dev] inst_subst_tac vs. 'a set

[Makarius]

Here is another change from 2008 to be reconsidered:

changeset:   26833:7c3757fccf0e
user:        berghofe
date:        Wed May 07 10:59:48 2008 +0200
files:       src/Provers/hypsubst.ML
description:
Added function for computing instantiation for the subst rule, which is used
in vars_gen_hyp_subst_tac and blast_hyp_subst_tac to avoid problems with
HO unification.


It is probably mainly relevant to Stefan and Larry.


 	Makarius