avoid stepping outside of context -- plain zero_var_indexes should be sufficient;

--- a/src/FOL/simpdata.ML	Mon Nov 28 12:13:27 2011 +0100
+++ b/src/FOL/simpdata.ML	Mon Nov 28 17:05:41 2011 +0100
@@ -27,7 +27,7 @@
 
 (*Congruence rules for = or <-> (instead of ==)*)
 fun mk_meta_cong ss rl =
-  Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
+  Drule.zero_var_indexes (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
     handle THM _ =>
       error("Premises and conclusion of congruence rules must use =-equality or <->");
 

--- 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 #>

--- a/src/Provers/typedsimp.ML	Mon Nov 28 12:13:27 2011 +0100
+++ b/src/Provers/typedsimp.ML	Mon Nov 28 17:05:41 2011 +0100
@@ -43,11 +43,11 @@
 (*For simplifying both sides of an equation:
       [| a=c; b=c |] ==> b=a
   Can use resolve_tac [split_eqn] to prepare an equation for simplification. *)
-val split_eqn = Drule.export_without_context (sym RSN (2,trans) RS sym);
+val split_eqn = Drule.zero_var_indexes (sym RSN (2,trans) RS sym);
 
 
 (*    [| a=b; b=c |] ==> reduce(a,c)  *)
-val red_trans = Drule.export_without_context (trans RS red_if_equal);
+val red_trans = Drule.zero_var_indexes (trans RS red_if_equal);
 
 (*For REWRITE rule: Make a reduction rule for simplification, e.g.
   [| a: C(0); ... ; a=c: C(0) |] ==> rec(0,a,b) = c: C(0) *)

--- a/src/Sequents/simpdata.ML	Mon Nov 28 12:13:27 2011 +0100
+++ b/src/Sequents/simpdata.ML	Mon Nov 28 17:05:41 2011 +0100
@@ -48,7 +48,7 @@
 
 (*Congruence rules for = or <-> (instead of ==)*)
 fun mk_meta_cong ss rl =
-  Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
+  Drule.zero_var_indexes (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
     handle THM _ =>
       error("Premises and conclusion of congruence rules must use =-equality or <->");