author | wenzelm |
Sun, 15 Jan 2012 14:22:54 +0100 | |
changeset 46223 | cf91e1944229 |
parent 46222 | cb3f370e66e1 |
child 46224 | 9cb98d34f593 |
--- a/src/HOL/Tools/record.ML Sun Jan 15 14:17:42 2012 +0100 +++ b/src/HOL/Tools/record.ML Sun Jan 15 14:22:54 2012 +0100 @@ -331,8 +331,8 @@ update_convs: thm list, select_defs: thm list, update_defs: thm list, - fold_congs: thm list, - unfold_congs: thm list, + fold_congs: thm list, (* FIXME unused!? *) + unfold_congs: thm list, (* FIXME unused!? *) splits: thm list, defs: thm list,