1.1 --- a/src/HOL/Tools/record.ML	Wed Nov 23 22:07:55 2011 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Wed Nov 23 22:59:39 2011 +0100
     1.3 @@ -515,8 +515,8 @@
     1.4          updates = fold Symtab.update_new upds updates,
     1.5          simpset = Simplifier.addsimps (simpset, simps),
     1.6          defset = Simplifier.addsimps (defset, defs),
     1.7 -        foldcong = foldcong addcongs folds,
     1.8 -        unfoldcong = unfoldcong addcongs unfolds}
     1.9 +        foldcong = foldcong |> fold Simplifier.add_cong folds,
    1.10 +        unfoldcong = unfoldcong |> fold Simplifier.add_cong unfolds}
    1.11         equalities extinjects extsplit splits extfields fieldext;
    1.12    in Data.put data thy end;
    1.13