src/Provers/hypsubst.ML

--- a/src/Provers/hypsubst.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Provers/hypsubst.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -223,7 +223,7 @@
   discarding equalities on Bound variables
   and on Free variables if thin=true*)
 fun hyp_subst_tac_thin thin ctxt =
-  REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
+  REPEAT_DETERM1 o FIRST' [ematch_tac ctxt [Data.thin_refl],
     gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac ctxt false,
     if thin then thin_free_eq_tac else K no_tac];