src/Provers/clasimp.ML
changeset 21963 416a5338d2bb
parent 21709 9cfd9eb9faec
child 22095 07875394618e
--- 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;