diff -r c2c647a4c237 -r 09539cdffcd7 src/Provers/hypsubst.ML
--- 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 #>