# HG changeset patch # User paulson # Date 962182040 -7200 # Node ID 88e0f647b9c23f915d41c8fb9eb138452eb946b7 # Parent 4d624e34e19a647ab8448dc24eb171c1cbccc334 make_elim -> cla_make_elim; tidied diff -r 4d624e34e19a -r 88e0f647b9c2 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Wed Jun 28 10:46:25 2000 +0200 +++ b/src/HOL/simpdata.ML Wed Jun 28 10:47:20 2000 +0200 @@ -36,17 +36,18 @@ fun delIff ((cla, simp), th) = (case HOLogic.dest_Trueprop (#prop (rep_thm th)) of - (Const ("Not", _) $ A) => - cla delrules [zero_var_indexes (th RS notE)] - | (con $ _ $ _) => - if con = iff_const - then cla delrules [zero_var_indexes (th RS iffD2), - make_elim (zero_var_indexes (th RS iffD1))] - else cla delrules [th] - | _ => cla delrules [th], + (Const ("Not", _) $ A) => + cla delrules [zero_var_indexes (th RS notE)] + | (con $ _ $ _) => + if con = iff_const + then cla delrules + [zero_var_indexes (th RS iffD2), + cla_make_elim (zero_var_indexes (th RS iffD1))] + else cla delrules [th] + | _ => cla delrules [th], simp delsimps [th]) handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ - string_of_thm th); (cla, simp)); + string_of_thm th); (cla, simp)); fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp) in