# HG changeset patch
# User wenzelm
# Date 1167491283 -3600
# Node ID 416a5338d2bb0122023357c4f952d4da2d15b75c
# Parent  279b129498b6f609633e9e639ddcfa6c605c43eb
removed obsolete name_hint handling;

diff -r 279b129498b6 -r 416a5338d2bb src/Provers/clasimp.ML
--- 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;
diff -r 279b129498b6 -r 416a5338d2bb 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;