# 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;