src/Provers/classical.ML
changeset 21646 c07b5b0e8492
parent 21516 c2a116a2c4fd
child 21687 f689f729afab
     1.1 --- a/src/Provers/classical.ML	Tue Dec 05 00:29:19 2006 +0100
     1.2 +++ b/src/Provers/classical.ML	Tue Dec 05 00:30:38 2006 +0100
     1.3 @@ -195,7 +195,7 @@
     1.4            else all_tac))
     1.5          |> Seq.hd
     1.6          |> Drule.zero_var_indexes
     1.7 -        |> Thm.put_name_tags (Thm.get_name_tags rule);
     1.8 +        |> PureThy.put_name_hint (PureThy.get_name_hint rule);
     1.9      in if Drule.equiv_thm (rule, rule'') then rule else rule'' end
    1.10    else rule;
    1.11  
    1.12 @@ -424,9 +424,9 @@
    1.13      if has_fewer_prems 1 th then
    1.14      	error("Ill-formed destruction rule\n" ^ string_of_thm th)
    1.15      else
    1.16 -    case Thm.name_of_thm th of
    1.17 +    case PureThy.get_name_hint th of
    1.18          "" => Tactic.make_elim th
    1.19 -      | a  => Thm.name_thm (a ^ "_dest", Tactic.make_elim th);
    1.20 +      | a  => PureThy.put_name_hint (a ^ "_dest") (Tactic.make_elim th);
    1.21  
    1.22  fun cs addSDs ths = cs addSEs (map name_make_elim ths);
    1.23