preservation of names

--- a/src/Provers/classical.ML	Wed Jan 04 16:13:53 2006 +0100
+++ b/src/Provers/classical.ML	Wed Jan 04 16:14:15 2006 +0100
@@ -204,6 +204,7 @@
 fun classical_rule rule =
   if is_elim rule then
     let
+      val ntags = Thm.get_name_tags rule;
       val rule' = rule RS classical;
       val concl' = Thm.concl_of rule';
       fun redundant_hyp goal =
@@ -217,7 +218,8 @@
           then Tactic.etac thin_rl i
           else all_tac))
         |> Seq.hd
-        |> Drule.zero_var_indexes;
+        |> Drule.zero_var_indexes
+        |> Thm.put_name_tags ntags;
     in if Drule.weak_eq_thm (rule, rule'') then rule else rule'' end
   else rule;