# HG changeset patch
# User paulson
# Date 1165506374 -3600
# Node ID 58abd6d8abd13b3c7faacb733648cb8019983df8
# Parent  e5287f12f1e10046f38481a4f4b80e59604f1b6c
Removal of theorem tagging, which the ATP linkup no longer requires,

diff -r e5287f12f1e1 -r 58abd6d8abd1 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Thu Dec 07 14:11:39 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Thu Dec 07 16:46:14 2006 +0100
@@ -298,11 +298,6 @@
 
 end;
 
-(*Name management for ATP linkup. The suffix here must agree with the one given
-  for notE in Clasimp.addIff*)
-fun name_notE th =
-  PureThy.put_name_hint (PureThy.get_name_hint th ^ "_iff1") (th RS notE);
-      
 fun add_rules simps case_thms size_thms rec_thms inject distinct
                   weak_case_congs cong_att =
   PureThy.add_thmss [(("simps", simps), []),
@@ -310,7 +305,7 @@
           flat distinct @ rec_thms), [Simplifier.simp_add]),
     (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
     (("", flat inject), [iff_add]),
-    (("", map name_notE (flat distinct)), [Classical.safe_elim NONE]),
+    (("", map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
     (("", weak_case_congs), [cong_att])]
   #> snd;
 
diff -r e5287f12f1e1 -r 58abd6d8abd1 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Dec 07 14:11:39 2006 +0100
+++ b/src/Provers/classical.ML	Thu Dec 07 16:46:14 2006 +0100
@@ -419,16 +419,12 @@
 fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
 fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
 
-(*Give new theorem a name, if it has one already.*)
-fun name_make_elim th =
+fun make_elim th =
     if has_fewer_prems 1 th then
     	error("Ill-formed destruction rule\n" ^ string_of_thm th)
-    else
-    case PureThy.get_name_hint th of
-        "" => Tactic.make_elim th
-      | a  => PureThy.put_name_hint (a ^ "_dest") (Tactic.make_elim th);
+    else Tactic.make_elim th;
 
-fun cs addSDs ths = cs addSEs (map name_make_elim ths);
+fun cs addSDs ths = cs addSEs (map make_elim ths);
 
 
 (*** Hazardous (unsafe) rules ***)
@@ -488,7 +484,7 @@
 fun cs addIs ths = fold_rev (addI NONE) ths cs;
 fun cs addEs ths = fold_rev (addE NONE) ths cs;
 
-fun cs addDs ths = cs addEs (map name_make_elim ths);
+fun cs addDs ths = cs addEs (map make_elim ths);
 
 
 (*** Deletion of rules
@@ -936,10 +932,10 @@
    fn Context.Theory thy => (change_claset_of thy (f th); Context.Theory thy)
     | Context.Proof ctxt => Context.Proof (LocalClaset.map (f th) ctxt));
 
-fun safe_dest w = attrib (addSE w o name_make_elim);
+fun safe_dest w = attrib (addSE w o make_elim);
 val safe_elim = attrib o addSE;
 val safe_intro = attrib o addSI;
-fun haz_dest w = attrib (addE w o name_make_elim);
+fun haz_dest w = attrib (addE w o make_elim);
 val haz_elim = attrib o addE;
 val haz_intro = attrib o addI;
 val rule_del = attrib delrule o ContextRules.rule_del;