--- 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 =