Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Wed, 19 Jul 2006 12:12:02 +0200
changeset 20159 93a561cf000c
parent 20158 b71f4f4c6b1e
child 20160 550e36c6a2d1
tuned;
src/Pure/proofterm.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle