# HG changeset patch
# User wenzelm
# Date 1440761793 -7200
# Node ID 58e41aa1c36db45dc0e05da3b467481d5115b4fc
# Parent  d08a0c5a68f7840ab1b9f0f02242c0ec197f344e
tuned;

diff -r d08a0c5a68f7 -r 58e41aa1c36d src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Fri Aug 28 13:23:02 2015 +0200
+++ b/src/Pure/more_thm.ML	Fri Aug 28 13:36:33 2015 +0200
@@ -374,8 +374,8 @@
 
 fun forall_intr_frees th =
   let
-    val {prop, hyps, tpairs, ...} = Thm.rep_thm th;
-    val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) [];
+    val fixed =
+      fold Term.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th) @ Thm.hyps_of th) [];
     val frees =
       Thm.fold_atomic_cterms (fn a =>
         (case Thm.term_of a of