--- a/src/HOL/Tools/record_package.ML Fri Dec 05 11:42:27 2008 +0100
+++ b/src/HOL/Tools/record_package.ML Fri Dec 05 18:42:37 2008 +0100
@@ -346,19 +346,14 @@
val get_updates = Symtab.lookup o #updates o get_sel_upd;
fun get_simpset thy = Simplifier.theory_context thy (#simpset (get_sel_upd thy));
-fun put_sel_upd names simps thy =
- let
- val sels = map (rpair ()) names;
- val upds = map (suffix updateN) names ~~ names;
-
- val {records, sel_upd = {selectors, updates, simpset},
- equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy;
- val data = make_record_data records
- {selectors = Symtab.extend (selectors, sels),
- updates = Symtab.extend (updates, upds),
- simpset = Simplifier.addsimps (simpset, simps)}
- equalities extinjects extsplit splits extfields fieldext;
- in RecordsData.put data thy end;
+fun put_sel_upd names simps = RecordsData.map (fn {records,
+ sel_upd = {selectors, updates, simpset},
+ equalities, extinjects, extsplit, splits, extfields, fieldext} =>
+ make_record_data records
+ {selectors = fold (fn name => Symtab.update (name, ())) names selectors,
+ updates = fold (fn name => Symtab.update ((suffix updateN) name, name)) names updates,
+ simpset = Simplifier.addsimps (simpset, simps)}
+ equalities extinjects extsplit splits extfields fieldext);
(* access 'equalities' *)