src/Provers/hypsubst.ML

 
 (*Substitutes for Free or Bound variables,
   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];
 
 val hyp_subst_thin = Attrib.setup_config_bool @{binding hypsubst_thin} (K false);