tuned;
authorwenzelm
Wed Jul 19 12:12:02 2006 +0200 (2006-07-19)
changeset 2015993a561cf000c
parent 20158 b71f4f4c6b1e
child 20160 550e36c6a2d1
tuned;
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/proofterm.ML	Wed Jul 19 12:12:01 2006 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Wed Jul 19 12:12:02 2006 +0200
     1.3 @@ -304,8 +304,8 @@
     1.4    | fold_proof_terms f g (prf % NONE) = fold_proof_terms f g prf
     1.5    | fold_proof_terms f g (prf1 %% prf2) =
     1.6        fold_proof_terms f g prf1 #> fold_proof_terms f g prf2
     1.7 -  | fold_proof_terms _ g (PThm (_, _, _, SOME Ts)) = fold g Ts  (* FIXME prop? *)
     1.8 -  | fold_proof_terms _ g (PAxm (_, prop, SOME Ts)) = fold g Ts  (* FIXME prop? *)
     1.9 +  | fold_proof_terms _ g (PThm (_, _, _, SOME Ts)) = fold g Ts
    1.10 +  | fold_proof_terms _ g (PAxm (_, _, SOME Ts)) = fold g Ts
    1.11    | fold_proof_terms _ _ _ = I;
    1.12  
    1.13  fun maxidx_of_proof prf = fold_proof_terms Term.maxidx_term Term.maxidx_typ prf ~1;