changeset 47095 | cf91e1944229 |
parent 47093 | 6dcb2cea827d |
child 47579 | b138dee7bed3 |
1.1 --- a/src/HOL/Tools/record.ML Sun Jan 15 14:17:42 2012 +0100 1.2 +++ b/src/HOL/Tools/record.ML Sun Jan 15 14:22:54 2012 +0100 1.3 @@ -331,8 +331,8 @@ 1.4 update_convs: thm list, 1.5 select_defs: thm list, 1.6 update_defs: thm list, 1.7 - fold_congs: thm list, 1.8 - unfold_congs: thm list, 1.9 + fold_congs: thm list, (* FIXME unused!? *) 1.10 + unfold_congs: thm list, (* FIXME unused!? *) 1.11 splits: thm list, 1.12 defs: thm list, 1.13