# HG changeset patch
# User paulson
# Date 1136809748 -3600
# Node ID 2db0982523fe51a9956bcd65482e5b97064257a4
# Parent  2e7afae14fa5fffe84573314eda8f493e40e90ef
_E suffix for compatibility with AddIffs

diff -r 2e7afae14fa5 -r 2db0982523fe src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Jan 09 13:28:34 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Mon Jan 09 13:29:08 2006 +0100
@@ -341,8 +341,10 @@
 
 end;
 
+(*Name management for ATP linkup. The suffix here must agree with the one given
+  for notE in Clasimp.addIff*)
 fun name_notE th =
-    Thm.name_thm (Thm.name_of_thm th ^ "_E", th RS notE);
+    Thm.name_thm (Thm.name_of_thm th ^ "_iff1", th RS notE);
       
 fun add_rules simps case_thms size_thms rec_thms inject distinct
                   weak_case_congs cong_att =