removed obsolete name_hint handling;

--- a/src/Provers/clasimp.ML	Sat Dec 30 16:08:00 2006 +0100
+++ b/src/Provers/clasimp.ML	Sat Dec 30 16:08:03 2006 +0100
@@ -125,7 +125,6 @@
 
 fun addIff decls1 decls2 simp ((cs, ss), th) =
   let
-    val name = PureThy.get_name_hint th;
     val n = nprems_of th;
     val (elim, intro) = if n = 0 then decls1 else decls2;
     val zero_rotate = zero_var_indexes o rotate_prems n;

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