src/HOL/Tools/datatype_package.ML
changeset 18625 2db0982523fe
parent 18518 3b1dfa53e64f
child 18643 89a7978f90e1
--- 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 =