src/HOL/cladata.ML
changeset 12355 c8d3c3d09080
parent 11753 02b257ef0ee2
child 15570 8d8c70b41bab
     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);