| changeset 35021 | c839a4c670c6 |
| parent 32957 | 675c0c7e6a37 |
| child 35232 | f588e1169c8b |
--- a/src/Provers/hypsubst.ML Sun Feb 07 19:31:55 2010 +0100 +++ b/src/Provers/hypsubst.ML Sun Feb 07 19:33:34 2010 +0100 @@ -165,7 +165,7 @@ end; -val ssubst = Drule.standard (Data.sym RS Data.subst); +val ssubst = Drule.export_without_context (Data.sym RS Data.subst); fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) => case try (Logic.strip_assums_hyp #> hd #>