# HG changeset patch
# User paulson
# Date 1165581626 -3600
# Node ID 9cfd9eb9faec5fcf2d8eccbf4bb9d801629a7572
# Parent  45e7491bea47e07d9eff68a38f446315c739249b
removed use of put_name_hint, as the ATP linkup no longer needs this

diff -r 45e7491bea47 -r 9cfd9eb9faec src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Thu Dec 07 23:16:55 2006 +0100
+++ b/src/Provers/clasimp.ML	Fri Dec 08 13:40:26 2006 +0100
@@ -114,10 +114,6 @@
 fun cs addss' ss = Classical.addbefore  (cs, ("asm_full_simp_tac",
                             CHANGED o Simplifier.asm_lr_simp_tac ss));
 
-(*Attach a suffix, provided we have a name to start with.*)
-fun suffix_thm "" _ = I
-  | suffix_thm a b = PureThy.put_name_hint (a^b);
-
 (* iffs: addition of rules to simpsets and clasets simultaneously *)
 
 (*Takes (possibly conditional) theorems of the form A<->B to
@@ -134,9 +130,9 @@
     val (elim, intro) = if n = 0 then decls1 else decls2;
     val zero_rotate = zero_var_indexes o rotate_prems n;
   in
-    (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS iffD2))]),
-           [suffix_thm name "_iff1" (Tactic.make_elim (zero_rotate (th RS iffD1)))])
-      handle THM _ => (elim (cs, [suffix_thm name "_iff1" (zero_rotate (th RS notE))])
+    (elim (intro (cs, [zero_rotate (th RS iffD2)]),
+           [Tactic.make_elim (zero_rotate (th RS iffD1))])
+      handle THM _ => (elim (cs, [zero_rotate (th RS notE)])
         handle THM _ => intro (cs, [th])),
      simp (ss, [th]))
   end;