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