--- 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;