author | wenzelm |
Thu, 26 Apr 2012 20:22:39 +0200 | |
changeset 47783 | 0eadfb89badb |
parent 47782 | 1678955ca991 |
child 47784 | fe43977e434f |
--- 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,