Removal of theorem tagging, which the ATP linkup no longer requires,
authorpaulson
Thu Dec 07 16:46:14 2006 +0100 (2006-12-07)
changeset 2168958abd6d8abd1
parent 21688 e5287f12f1e1
child 21690 552d20ff9a95
Removal of theorem tagging, which the ATP linkup no longer requires,
src/HOL/Tools/datatype_package.ML
src/Provers/classical.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Dec 07 14:11:39 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Dec 07 16:46:14 2006 +0100
     1.3 @@ -298,11 +298,6 @@
     1.4  
     1.5  end;
     1.6  
     1.7 -(*Name management for ATP linkup. The suffix here must agree with the one given
     1.8 -  for notE in Clasimp.addIff*)
     1.9 -fun name_notE th =
    1.10 -  PureThy.put_name_hint (PureThy.get_name_hint th ^ "_iff1") (th RS notE);
    1.11 -      
    1.12  fun add_rules simps case_thms size_thms rec_thms inject distinct
    1.13                    weak_case_congs cong_att =
    1.14    PureThy.add_thmss [(("simps", simps), []),
    1.15 @@ -310,7 +305,7 @@
    1.16            flat distinct @ rec_thms), [Simplifier.simp_add]),
    1.17      (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
    1.18      (("", flat inject), [iff_add]),
    1.19 -    (("", map name_notE (flat distinct)), [Classical.safe_elim NONE]),
    1.20 +    (("", map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
    1.21      (("", weak_case_congs), [cong_att])]
    1.22    #> snd;
    1.23  
     2.1 --- a/src/Provers/classical.ML	Thu Dec 07 14:11:39 2006 +0100
     2.2 +++ b/src/Provers/classical.ML	Thu Dec 07 16:46:14 2006 +0100
     2.3 @@ -419,16 +419,12 @@
     2.4  fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
     2.5  fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
     2.6  
     2.7 -(*Give new theorem a name, if it has one already.*)
     2.8 -fun name_make_elim th =
     2.9 +fun make_elim th =
    2.10      if has_fewer_prems 1 th then
    2.11      	error("Ill-formed destruction rule\n" ^ string_of_thm th)
    2.12 -    else
    2.13 -    case PureThy.get_name_hint th of
    2.14 -        "" => Tactic.make_elim th
    2.15 -      | a  => PureThy.put_name_hint (a ^ "_dest") (Tactic.make_elim th);
    2.16 +    else Tactic.make_elim th;
    2.17  
    2.18 -fun cs addSDs ths = cs addSEs (map name_make_elim ths);
    2.19 +fun cs addSDs ths = cs addSEs (map make_elim ths);
    2.20  
    2.21  
    2.22  (*** Hazardous (unsafe) rules ***)
    2.23 @@ -488,7 +484,7 @@
    2.24  fun cs addIs ths = fold_rev (addI NONE) ths cs;
    2.25  fun cs addEs ths = fold_rev (addE NONE) ths cs;
    2.26  
    2.27 -fun cs addDs ths = cs addEs (map name_make_elim ths);
    2.28 +fun cs addDs ths = cs addEs (map make_elim ths);
    2.29  
    2.30  
    2.31  (*** Deletion of rules
    2.32 @@ -936,10 +932,10 @@
    2.33     fn Context.Theory thy => (change_claset_of thy (f th); Context.Theory thy)
    2.34      | Context.Proof ctxt => Context.Proof (LocalClaset.map (f th) ctxt));
    2.35  
    2.36 -fun safe_dest w = attrib (addSE w o name_make_elim);
    2.37 +fun safe_dest w = attrib (addSE w o make_elim);
    2.38  val safe_elim = attrib o addSE;
    2.39  val safe_intro = attrib o addSI;
    2.40 -fun haz_dest w = attrib (addE w o name_make_elim);
    2.41 +fun haz_dest w = attrib (addE w o make_elim);
    2.42  val haz_elim = attrib o addE;
    2.43  val haz_intro = attrib o addI;
    2.44  val rule_del = attrib delrule o ContextRules.rule_del;