| changeset 45659 | 09539cdffcd7 |
| parent 45625 | 750c5a47400b |
| child 46219 | 426ed18eba43 |
--- a/src/Provers/hypsubst.ML Mon Nov 28 12:13:27 2011 +0100 +++ b/src/Provers/hypsubst.ML Mon Nov 28 17:05:41 2011 +0100 @@ -139,7 +139,7 @@ end; -val ssubst = Drule.export_without_context (Data.sym RS Data.subst); +val ssubst = Drule.zero_var_indexes (Data.sym RS Data.subst); fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) => case try (Logic.strip_assums_hyp #> hd #>