diff -r 5c5b5c7f1157 -r a9873318fe30 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Fri Apr 30 17:18:29 2010 +0200
+++ b/src/FOL/simpdata.ML	Fri Apr 30 18:06:29 2010 +0200
@@ -21,13 +21,13 @@
   | _                           => th RS @{thm iff_reflection_T};
 
 (*Replace premises x=y, X<->Y by X==Y*)
-val mk_meta_prems =
-    rule_by_tactic
+fun mk_meta_prems ctxt =
+    rule_by_tactic ctxt
       (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
 
 (*Congruence rules for = or <-> (instead of ==)*)
-fun mk_meta_cong (_: simpset) rl =
-  Drule.export_without_context (mk_meta_eq (mk_meta_prems rl))
+fun mk_meta_cong ss rl =
+  Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl))
     handle THM _ =>
       error("Premises and conclusion of congruence rules must use =-equality or <->");