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;