src/HOL/simpdata.ML
changeset 9164 88e0f647b9c2
parent 9023 09d02e7365c1
child 9384 8e8941c491e6
     1.1 --- a/src/HOL/simpdata.ML	Wed Jun 28 10:46:25 2000 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Wed Jun 28 10:47:20 2000 +0200
     1.3 @@ -36,17 +36,18 @@
     1.4  
     1.5    fun delIff ((cla, simp), th) = 
     1.6        (case HOLogic.dest_Trueprop (#prop (rep_thm th)) of
     1.7 -                (Const ("Not", _) $ A) =>
     1.8 -                    cla delrules [zero_var_indexes (th RS notE)]
     1.9 -              | (con $ _ $ _) =>
    1.10 -                    if con = iff_const
    1.11 -                    then cla delrules [zero_var_indexes (th RS iffD2),
    1.12 -                                       make_elim (zero_var_indexes (th RS iffD1))]
    1.13 -                    else cla delrules [th]
    1.14 -              | _ => cla delrules [th],
    1.15 +	   (Const ("Not", _) $ A) =>
    1.16 +	       cla delrules [zero_var_indexes (th RS notE)]
    1.17 +	 | (con $ _ $ _) =>
    1.18 +	       if con = iff_const
    1.19 +	       then cla delrules 
    1.20 +		        [zero_var_indexes (th RS iffD2),
    1.21 +			 cla_make_elim (zero_var_indexes (th RS iffD1))]
    1.22 +	       else cla delrules [th]
    1.23 +	 | _ => cla delrules [th],
    1.24         simp delsimps [th])
    1.25        handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ 
    1.26 -                          string_of_thm th); (cla, simp));
    1.27 +				string_of_thm th); (cla, simp));
    1.28  
    1.29    fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)
    1.30  in