hyp_subst_tac';
authorwenzelm
Tue Dec 04 02:01:31 2001 +0100 (2001-12-04)
changeset 12355c8d3c3d09080
parent 12354 5f5ee25513c5
child 12356 ce0961b1f536
hyp_subst_tac';
src/HOL/cladata.ML
     1.1 --- a/src/HOL/cladata.ML	Tue Dec 04 02:01:13 2001 +0100
     1.2 +++ b/src/HOL/cladata.ML	Tue Dec 04 02:01:31 2001 +0100
     1.3 @@ -30,6 +30,12 @@
     1.4  structure Hypsubst = HypsubstFun(Hypsubst_Data);
     1.5  open Hypsubst;
     1.6  
     1.7 +(*prevent substitution on bool*)
     1.8 +fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso
     1.9 +  Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", []) | _ => false)
    1.10 +    (Library.nth_elem (i - 1, Thm.prems_of thm)) then hyp_subst_tac i thm else no_tac thm;
    1.11 +
    1.12 +
    1.13  
    1.14  (*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
    1.15  structure Make_Elim = Make_Elim_Fun (val classical = classical);