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