src/Provers/classical.ML
changeset 21689 58abd6d8abd1
parent 21687 f689f729afab
child 21963 416a5338d2bb
     1.1 --- a/src/Provers/classical.ML	Thu Dec 07 14:11:39 2006 +0100
     1.2 +++ b/src/Provers/classical.ML	Thu Dec 07 16:46:14 2006 +0100
     1.3 @@ -419,16 +419,12 @@
     1.4  fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
     1.5  fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
     1.6  
     1.7 -(*Give new theorem a name, if it has one already.*)
     1.8 -fun name_make_elim th =
     1.9 +fun make_elim th =
    1.10      if has_fewer_prems 1 th then
    1.11      	error("Ill-formed destruction rule\n" ^ string_of_thm th)
    1.12 -    else
    1.13 -    case PureThy.get_name_hint th of
    1.14 -        "" => Tactic.make_elim th
    1.15 -      | a  => PureThy.put_name_hint (a ^ "_dest") (Tactic.make_elim th);
    1.16 +    else Tactic.make_elim th;
    1.17  
    1.18 -fun cs addSDs ths = cs addSEs (map name_make_elim ths);
    1.19 +fun cs addSDs ths = cs addSEs (map make_elim ths);
    1.20  
    1.21  
    1.22  (*** Hazardous (unsafe) rules ***)
    1.23 @@ -488,7 +484,7 @@
    1.24  fun cs addIs ths = fold_rev (addI NONE) ths cs;
    1.25  fun cs addEs ths = fold_rev (addE NONE) ths cs;
    1.26  
    1.27 -fun cs addDs ths = cs addEs (map name_make_elim ths);
    1.28 +fun cs addDs ths = cs addEs (map make_elim ths);
    1.29  
    1.30  
    1.31  (*** Deletion of rules
    1.32 @@ -936,10 +932,10 @@
    1.33     fn Context.Theory thy => (change_claset_of thy (f th); Context.Theory thy)
    1.34      | Context.Proof ctxt => Context.Proof (LocalClaset.map (f th) ctxt));
    1.35  
    1.36 -fun safe_dest w = attrib (addSE w o name_make_elim);
    1.37 +fun safe_dest w = attrib (addSE w o make_elim);
    1.38  val safe_elim = attrib o addSE;
    1.39  val safe_intro = attrib o addSI;
    1.40 -fun haz_dest w = attrib (addE w o name_make_elim);
    1.41 +fun haz_dest w = attrib (addE w o make_elim);
    1.42  val haz_elim = attrib o addE;
    1.43  val haz_intro = attrib o addI;
    1.44  val rule_del = attrib delrule o ContextRules.rule_del;