# 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