# HG changeset patch
# User berghofe
# Date 1275382118 -7200
# Node ID 4bbda9fc26db2c4b2c41d2bd0f2590ed06a8cbc3
# Parent  bdd8dd217b1fd27f44b37464b937db96ed1585bc
Use Proofterm.forall_intr_proof' instead of locally defined forall_intr_prf.

diff -r bdd8dd217b1f -r 4bbda9fc26db src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Tue Jun 01 10:46:47 2010 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Tue Jun 01 10:48:38 2010 +0200
@@ -28,11 +28,7 @@
 fun forall_intr_vfs prop = fold_rev Logic.all
   (vars_of prop @ frees_of prop) prop;
 
-fun forall_intr_prf t prf =
-  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
-  in Abst (a, SOME T, prf_abstract_over t prf) end;
-
-fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_prf
+fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof'
   (vars_of prop @ frees_of prop) prf;