# HG changeset patch
# User oheimb
# Date 991320722 -7200
# Node ID 57b7ad51971c05a7ab884544a2e0d0a22fb1b18d
# Parent  d5f1b482bfbfdf338e0bea14bc676b821be100af
streamlined addIffs/delIffs, added warnings

diff -r d5f1b482bfbf -r 57b7ad51971c src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Thu May 31 16:51:26 2001 +0200
+++ b/src/FOL/simpdata.ML	Thu May 31 16:52:02 2001 +0200
@@ -359,9 +359,7 @@
 structure Clasimp = ClasimpFun
  (structure Simplifier = Simplifier and Splitter = Splitter
   and Classical  = Cla and Blast = Blast
-  val dest_Trueprop = FOLogic.dest_Trueprop
-  val iff_const = FOLogic.iff val not_const = FOLogic.not
-  val notE = notE val iffD1 = iffD1 val iffD2 = iffD2
+  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE
   val cla_make_elim = cla_make_elim);
 open Clasimp;
 
diff -r d5f1b482bfbf -r 57b7ad51971c src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu May 31 16:51:26 2001 +0200
+++ b/src/HOL/simpdata.ML	Thu May 31 16:52:02 2001 +0200
@@ -454,10 +454,7 @@
 structure Clasimp = ClasimpFun
  (structure Simplifier = Simplifier and Splitter = Splitter
   and Classical  = Classical and Blast = Blast
-  val dest_Trueprop = HOLogic.dest_Trueprop
-  val iff_const = HOLogic.eq_const HOLogic.boolT
-  val not_const = HOLogic.not_const
-  val notE = notE val iffD1 = iffD1 val iffD2 = iffD2
+  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE
   val cla_make_elim = cla_make_elim);
 open Clasimp;
 
diff -r d5f1b482bfbf -r 57b7ad51971c src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Thu May 31 16:51:26 2001 +0200
+++ b/src/Provers/clasimp.ML	Thu May 31 16:52:02 2001 +0200
@@ -16,9 +16,6 @@
   structure Classical: CLASSICAL
   structure Blast: BLAST
   sharing type Classical.claset = Blast.claset
-  val dest_Trueprop: term -> term
-  val not_const: term
-  val iff_const: term
   val notE: thm
   val iffD1: thm
   val iffD2: thm
@@ -116,39 +113,30 @@
 
 (* iffs: addition of rules to simpsets and clasets simultaneously *)
 
-(*Takes UNCONDITIONAL theorems of the form A<->B to
+(*Takes (possibly conditional) theorems of the form A<->B to
         the Safe Intr     rule B==>A and
         the Safe Destruct rule A==>B.
   Also ~A goes to the Safe Elim rule A ==> ?R
-  Failing other cases, A is added as a Safe Intr rule*)
+  Failing other cases, A is added as a Safe Intr rule and a warning is issued *)
 local
 
 fun addIff dest elim intro simp ((cs, ss), th) =
-  (case dest_Trueprop (#prop (Thm.rep_thm th)) of
-    con $ _ $ _ =>
-      if con = Data.iff_const then
-        dest (intro (cs, [zero_var_indexes (th RS Data.iffD2)]),
-          [zero_var_indexes (th RS Data.iffD1)])
-      else intro (cs, [th])
-  | con $ A =>
-      if con = Data.not_const then elim (cs, [zero_var_indexes (th RS Data.notE)])
-      else intro (cs, [th])
-  | _ => intro (cs, [th]), simp (ss, [th]))
-  handle TERM _ => error ("iff add: theorem must be unconditional\n" ^ Display.string_of_thm th);
+  (          dest (intro (cs, [zero_var_indexes (th RS Data.iffD2)]),
+                              [zero_var_indexes (th RS Data.iffD1)])
+   handle THM _ => (warning ("iff add: theorem is not an equivalence\n" 
+                  ^ Display.string_of_thm th);
+                    elim (cs, [zero_var_indexes (th RS Data.notE )])
+   handle THM _ => intro (cs, [th])),
+   simp (ss, [th]));
 
 fun delIff ((cs, ss), th) =
-  (case dest_Trueprop (#prop (Thm.rep_thm th)) of
-    con $ _ $ _ =>
-      if con = Data.iff_const then
-        Classical.delrules (cs, [zero_var_indexes (th RS Data.iffD2),
-          Data.cla_make_elim (zero_var_indexes (th RS Data.iffD1))])
-      else Classical.delrules (cs, [th])
-  | con $ A =>
-      if con = Data.not_const then Classical.delrules (cs, [zero_var_indexes (th RS Data.notE)])
-      else Classical.delrules (cs, [th])
-  | _ => Classical.delrules (cs, [th]), Simplifier.delsimps (ss, [th]))
-  handle TERM _ =>
-    (warning ("iff del: ignoring conditional theorem\n" ^ string_of_thm th); (cs, ss));
+(                Classical.delrules (cs, [zero_var_indexes (th RS Data.iffD2),
+                      Data.cla_make_elim (zero_var_indexes (th RS Data.iffD1))])
+ handle THM _ => (warning ("iff del: theorem is not an equivalence\n" 
+                  ^ Display.string_of_thm th);
+                 Classical.delrules (cs, [zero_var_indexes (th RS Data.notE)])
+ handle THM _ => Classical.delrules (cs, [th])), 
+ Simplifier.delsimps (ss, [th]));
 
 fun store_clasimp (cs, ss) =
   (Classical.claset_ref () := cs; Simplifier.simpset_ref () := ss);