# HG changeset patch
# User wenzelm
# Date 1007427691 -3600
# Node ID c8d3c3d090808fea4cd6abd6a75f7810779d5ada
# Parent  5f5ee25513c51beb77c591f1ac6960b153a26ddd
hyp_subst_tac';

diff -r 5f5ee25513c5 -r c8d3c3d09080 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Tue Dec 04 02:01:13 2001 +0100
+++ b/src/HOL/cladata.ML	Tue Dec 04 02:01:31 2001 +0100
@@ -30,6 +30,12 @@
 structure Hypsubst = HypsubstFun(Hypsubst_Data);
 open Hypsubst;
 
+(*prevent substitution on bool*)
+fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso
+  Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", []) | _ => false)
+    (Library.nth_elem (i - 1, Thm.prems_of thm)) then hyp_subst_tac i thm else no_tac thm;
+
+
 
 (*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
 structure Make_Elim = Make_Elim_Fun (val classical = classical);