diff -r c2c647a4c237 -r 09539cdffcd7 src/Sequents/simpdata.ML
--- 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 <->");