src/HOL/Tools/datatype_package.ML
changeset 21646 c07b5b0e8492
parent 21459 20c2ddee8bc5
child 21689 58abd6d8abd1
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Dec 05 00:29:19 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Dec 05 00:30:38 2006 +0100
     1.3 @@ -301,7 +301,7 @@
     1.4  (*Name management for ATP linkup. The suffix here must agree with the one given
     1.5    for notE in Clasimp.addIff*)
     1.6  fun name_notE th =
     1.7 -    Thm.name_thm (Thm.name_of_thm th ^ "_iff1", th RS notE);
     1.8 +  PureThy.put_name_hint (PureThy.get_name_hint th ^ "_iff1") (th RS notE);
     1.9        
    1.10  fun add_rules simps case_thms size_thms rec_thms inject distinct
    1.11                    weak_case_congs cong_att =