tuned comment;
authorwenzelm
Thu, 26 Apr 2012 20:22:39 +0200
changeset 47783 0eadfb89badb
parent 47782 1678955ca991
child 47784 fe43977e434f
tuned comment;
src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu Apr 26 20:09:38 2012 +0200
+++ b/src/HOL/Tools/record.ML	Thu Apr 26 20:22:39 2012 +0200
@@ -331,8 +331,8 @@
   update_convs: thm list,
   select_defs: thm list,
   update_defs: thm list,
-  fold_congs: thm list,  (* FIXME unused!? *)
-  unfold_congs: thm list,  (* FIXME unused!? *)
+  fold_congs: thm list,  (* potentially used in L4.verified *)
+  unfold_congs: thm list,  (* potentially used in L4.verified *)
   splits: thm list,
   defs: thm list,