eliminated dead code;
authorwenzelm
Tue, 28 Jul 2015 21:31:16 +0200
changeset 60824 81bddc4832e6
parent 60823 b41478500473
child 60825 bacfb7c45d81
eliminated dead code;
src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Jul 28 21:10:41 2015 +0200
+++ b/src/Pure/more_thm.ML	Tue Jul 28 21:31:16 2015 +0200
@@ -364,7 +364,6 @@
 
 fun forall_intr_frees th =
   let
-    val thy = Thm.theory_of_thm th;
     val {prop, hyps, tpairs, ...} = Thm.rep_thm th;
     val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) [];
     val frees =