1.1 --- a/src/HOL/HOL.thy	Fri Feb 26 18:38:23 2010 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Feb 26 21:43:26 2010 +0100
     1.3 @@ -845,15 +845,16 @@
     1.4  
     1.5  setup {*
     1.6  let
     1.7 -  (*prevent substitution on bool*)
     1.8 -  fun hyp_subst_tac' i thm =
     1.9 -    if i <= Thm.nprems_of thm andalso
    1.10 -        Term.exists_Const
    1.11 -          (fn (@{const_name "op ="}, Type (_, [T, _])) => T <> @{typ bool} | _ => false)
    1.12 -          (nth (Thm.prems_of thm) (i - 1))
    1.13 -    then Hypsubst.hyp_subst_tac i thm else no_tac thm;
    1.14 +  fun non_bool_eq (@{const_name "op ="}, Type (_, [T, _])) = T <> @{typ bool}
    1.15 +    | non_bool_eq _ = false;
    1.16 +  val hyp_subst_tac' =
    1.17 +    SUBGOAL (fn (goal, i) =>
    1.18 +      if Term.exists_Const non_bool_eq goal
    1.19 +      then Hypsubst.hyp_subst_tac i
    1.20 +      else no_tac);
    1.21  in
    1.22    Hypsubst.hypsubst_setup
    1.23 +  (*prevent substitution on bool*)
    1.24    #> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
    1.25  end
    1.26  *}