src/HOL/HOL.thy
changeset 51798 ad3a241def73
parent 51717 9e7d1c139569
child 52143 36ffe23b25f8
     1.1 --- a/src/HOL/HOL.thy	Sat Apr 27 11:37:50 2013 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Apr 27 20:50:20 2013 +0200
     1.3 @@ -849,15 +849,15 @@
     1.4  let
     1.5    fun non_bool_eq (@{const_name HOL.eq}, Type (_, [T, _])) = T <> @{typ bool}
     1.6      | non_bool_eq _ = false;
     1.7 -  val hyp_subst_tac' =
     1.8 +  fun hyp_subst_tac' ctxt =
     1.9      SUBGOAL (fn (goal, i) =>
    1.10        if Term.exists_Const non_bool_eq goal
    1.11 -      then Hypsubst.hyp_subst_tac i
    1.12 +      then Hypsubst.hyp_subst_tac ctxt i
    1.13        else no_tac);
    1.14  in
    1.15    Hypsubst.hypsubst_setup
    1.16    (*prevent substitution on bool*)
    1.17 -  #> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
    1.18 +  #> Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac' ctxt ORELSE' tac)
    1.19  end
    1.20  *}
    1.21