src/HOL/Tools/record.ML
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