Use Proofterm.forall_intr_proof' instead of locally defined forall_intr_prf.

--- 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;