diff -r 0c5cd369a643 -r 50b60f501b05 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Tools/simpdata.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -79,13 +79,15 @@
   end;
 
 (*Congruence rules for = (instead of ==)*)
-fun mk_meta_cong (_: Proof.context) rl = zero_var_indexes
-  (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
-     resolve_tac [lift_meta_eq_to_obj_eq i st] i st) rl)
-   in mk_meta_eq rl' handle THM _ =>
-     if can Logic.dest_equals (concl_of rl') then rl'
-     else error "Conclusion of congruence rules must be =-equality"
-   end);
+fun mk_meta_cong ctxt rl =
+  let
+    val rl' = Seq.hd (TRYALL (fn i => fn st =>
+      resolve_tac ctxt [lift_meta_eq_to_obj_eq i st] i st) rl)
+  in
+    mk_meta_eq rl' handle THM _ =>
+      if can Logic.dest_equals (concl_of rl') then rl'
+      else error "Conclusion of congruence rules must be =-equality"
+  end |> zero_var_indexes;
 
 fun mk_atomize ctxt pairs =
   let
@@ -120,7 +122,10 @@
     val sol_thms =
       reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
     fun sol_tac i =
-      FIRST [resolve_tac sol_thms i, assume_tac ctxt i , eresolve_tac @{thms FalseE} i] ORELSE
+      FIRST
+       [resolve_tac ctxt sol_thms i,
+        assume_tac ctxt i,
+        eresolve_tac ctxt @{thms FalseE} i] ORELSE
       (match_tac ctxt intros THEN_ALL_NEW sol_tac) i
   in
     (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN' sol_tac