# HG changeset patch
# User wenzelm
# Date 1438111876 -7200
# Node ID 81bddc4832e698f0f4bcd3727d8d8cf452be9a2a
# Parent  b4147850047307ecd9c0e039a9d271e33490a226
eliminated dead code;

diff -r b41478500473 -r 81bddc4832e6 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 =