# HG changeset patch
# User paulson
# Date 1136387655 -3600
# Node ID 4927aa1feb232a819a9eb5fb1089b9ba046143d4
# Parent  ffce25f9aa7f7fa30ebd2ce7ec77e6b6e512c475
preservation of names

diff -r ffce25f9aa7f -r 4927aa1feb23 src/Provers/classical.ML
--- 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;