src/FOL/intprover.ML

--- a/src/FOL/intprover.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOL/intprover.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -66,9 +66,9 @@
   FIRST' [
     eq_assume_tac,
     eq_mp_tac,
-    bimatch_tac safe0_brls,
+    bimatch_tac ctxt safe0_brls,
     hyp_subst_tac ctxt,
-    bimatch_tac safep_brls];
+    bimatch_tac ctxt safep_brls];
 
 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
 fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt);