# HG changeset patch
# User wenzelm
# Date 1267217006 -3600
# Node ID 2be5440f7271eb7918faa90a2c5e3c2e98b4a496
# Parent  42d39948cace08bcc9f677c0cfde6fc15f69c3b9
tuned hyp_subst_tac';

diff -r 42d39948cace -r 2be5440f7271 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Feb 26 18:38:23 2010 +0100
+++ b/src/HOL/HOL.thy	Fri Feb 26 21:43:26 2010 +0100
@@ -845,15 +845,16 @@
 
 setup {*
 let
-  (*prevent substitution on bool*)
-  fun hyp_subst_tac' i thm =
-    if i <= Thm.nprems_of thm andalso
-        Term.exists_Const
-          (fn (@{const_name "op ="}, Type (_, [T, _])) => T <> @{typ bool} | _ => false)
-          (nth (Thm.prems_of thm) (i - 1))
-    then Hypsubst.hyp_subst_tac i thm else no_tac thm;
+  fun non_bool_eq (@{const_name "op ="}, Type (_, [T, _])) = T <> @{typ bool}
+    | non_bool_eq _ = false;
+  val hyp_subst_tac' =
+    SUBGOAL (fn (goal, i) =>
+      if Term.exists_Const non_bool_eq goal
+      then Hypsubst.hyp_subst_tac i
+      else no_tac);
 in
   Hypsubst.hypsubst_setup
+  (*prevent substitution on bool*)
   #> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
 end
 *}