1.1 --- a/src/Pure/Proof/reconstruct.ML	Tue Jun 01 10:46:47 2010 +0200
     1.2 +++ b/src/Pure/Proof/reconstruct.ML	Tue Jun 01 10:48:38 2010 +0200
     1.3 @@ -28,11 +28,7 @@
     1.4  fun forall_intr_vfs prop = fold_rev Logic.all
     1.5    (vars_of prop @ frees_of prop) prop;
     1.6  
     1.7 -fun forall_intr_prf t prf =
     1.8 -  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
     1.9 -  in Abst (a, SOME T, prf_abstract_over t prf) end;
    1.10 -
    1.11 -fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_prf
    1.12 +fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof'
    1.13    (vars_of prop @ frees_of prop) prf;
    1.14  
    1.15