src/Provers/classical.ML

--- a/src/Provers/classical.ML	Sat Dec 30 16:08:00 2006 +0100
+++ b/src/Provers/classical.ML	Sat Dec 30 16:08:03 2006 +0100
@@ -194,8 +194,7 @@
           then Tactic.etac thin_rl i
           else all_tac))
         |> Seq.hd
-        |> Drule.zero_var_indexes
-        |> PureThy.put_name_hint (PureThy.get_name_hint rule);
+        |> Drule.zero_var_indexes;
     in if Drule.equiv_thm (rule, rule'') then rule else rule'' end
   else rule;