src/Pure/Proof/reconstruct.ML
changeset 23178 07ba6b58b3d2
parent 21646 c07b5b0e8492
child 25246 584d8f2e1fc9
     1.1 --- a/src/Pure/Proof/reconstruct.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Pure/Proof/reconstruct.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -26,19 +26,19 @@
     1.4  fun vars_of t = rev (fold_aterms
     1.5    (fn v as Var _ => insert (op =) v | _ => I) t []);
     1.6  
     1.7 -fun forall_intr (t, prop) =
     1.8 +fun forall_intr t prop =
     1.9    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    1.10    in all T $ Abs (a, T, abstract_over (t, prop)) end;
    1.11  
    1.12 -fun forall_intr_vfs prop = foldr forall_intr prop
    1.13 -  (vars_of prop @ sort Term.term_ord (term_frees prop));
    1.14 +fun forall_intr_vfs prop = fold_rev forall_intr
    1.15 +  (vars_of prop @ sort Term.term_ord (term_frees prop)) prop;
    1.16  
    1.17 -fun forall_intr_prf (t, prf) =
    1.18 +fun forall_intr_prf t prf =
    1.19    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    1.20    in Abst (a, SOME T, prf_abstract_over t prf) end;
    1.21  
    1.22 -fun forall_intr_vfs_prf prop prf = foldr forall_intr_prf prf
    1.23 -  (vars_of prop @ sort Term.term_ord (term_frees prop));
    1.24 +fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_prf
    1.25 +  (vars_of prop @ sort Term.term_ord (term_frees prop)) prf;
    1.26  
    1.27  fun merge_envs (Envir.Envir {asol=asol1, iTs=iTs1, maxidx=maxidx1})
    1.28    (Envir.Envir {asol=asol2, iTs=iTs2, maxidx=maxidx2}) =
    1.29 @@ -49,7 +49,7 @@
    1.30  
    1.31  (**** generate constraints for proof term ****)
    1.32  
    1.33 -fun mk_var env Ts T = 
    1.34 +fun mk_var env Ts T =
    1.35    let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T)
    1.36    in (env', list_comb (v, map Bound (length Ts - 1 downto 0))) end;
    1.37  
    1.38 @@ -74,7 +74,7 @@
    1.39  fun infer_type thy (env as Envir.Envir {maxidx, asol, iTs}) Ts vTs
    1.40        (t as Const (s, T)) = if T = dummyT then (case Sign.const_type thy s of
    1.41            NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
    1.42 -        | SOME T => 
    1.43 +        | SOME T =>
    1.44              let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T)
    1.45              in (Const (s, T'), T', vTs,
    1.46                Envir.Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs})
    1.47 @@ -156,7 +156,7 @@
    1.48  
    1.49      fun head_norm (prop, prf, cnstrts, env, vTs) =
    1.50        (Envir.head_norm env prop, prf, cnstrts, env, vTs);
    1.51 - 
    1.52 +
    1.53      fun mk_cnstrts env _ Hs vTs (PBound i) = (List.nth (Hs, i), PBound i, [], env, vTs)
    1.54        | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) =
    1.55            let
    1.56 @@ -338,10 +338,10 @@
    1.57  
    1.58  fun expand_proof thy thms prf =
    1.59    let
    1.60 -    fun expand maxidx prfs (AbsP (s, t, prf)) = 
    1.61 +    fun expand maxidx prfs (AbsP (s, t, prf)) =
    1.62            let val (maxidx', prfs', prf') = expand maxidx prfs prf
    1.63            in (maxidx', prfs', AbsP (s, t, prf')) end
    1.64 -      | expand maxidx prfs (Abst (s, T, prf)) = 
    1.65 +      | expand maxidx prfs (Abst (s, T, prf)) =
    1.66            let val (maxidx', prfs', prf') = expand maxidx prfs prf
    1.67            in (maxidx', prfs', Abst (s, T, prf')) end
    1.68        | expand maxidx prfs (prf1 %% prf2) =