# HG changeset patch
# User wenzelm
# Date 1153303922 -7200
# Node ID 93a561cf000ccd30ee9e30f21e7258b5148d7eb7
# Parent  b71f4f4c6b1ec33e66a3f91d2614f550508c9315
tuned;

diff -r b71f4f4c6b1e -r 93a561cf000c src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Jul 19 12:12:01 2006 +0200
+++ b/src/Pure/proofterm.ML	Wed Jul 19 12:12:02 2006 +0200
@@ -304,8 +304,8 @@
   | fold_proof_terms f g (prf % NONE) = fold_proof_terms f g prf
   | fold_proof_terms f g (prf1 %% prf2) =
       fold_proof_terms f g prf1 #> fold_proof_terms f g prf2
-  | fold_proof_terms _ g (PThm (_, _, _, SOME Ts)) = fold g Ts  (* FIXME prop? *)
-  | fold_proof_terms _ g (PAxm (_, prop, SOME Ts)) = fold g Ts  (* FIXME prop? *)
+  | fold_proof_terms _ g (PThm (_, _, _, SOME Ts)) = fold g Ts
+  | fold_proof_terms _ g (PAxm (_, _, SOME Ts)) = fold g Ts
   | fold_proof_terms _ _ _ = I;
 
 fun maxidx_of_proof prf = fold_proof_terms Term.maxidx_term Term.maxidx_typ prf ~1;