src/HOL/Tools/record_package.ML
changeset 29004 a5a91f387791
parent 28965 1de908189869
child 29064 70a61d58460e
     1.1 --- a/src/HOL/Tools/record_package.ML	Fri Dec 05 11:42:27 2008 +0100
     1.2 +++ b/src/HOL/Tools/record_package.ML	Fri Dec 05 18:42:37 2008 +0100
     1.3 @@ -346,19 +346,14 @@
     1.4  val get_updates = Symtab.lookup o #updates o get_sel_upd;
     1.5  fun get_simpset thy = Simplifier.theory_context thy (#simpset (get_sel_upd thy));
     1.6  
     1.7 -fun put_sel_upd names simps thy =
     1.8 -  let
     1.9 -    val sels = map (rpair ()) names;
    1.10 -    val upds = map (suffix updateN) names ~~ names;
    1.11 -
    1.12 -    val {records, sel_upd = {selectors, updates, simpset},
    1.13 -      equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy;
    1.14 -    val data = make_record_data records
    1.15 -      {selectors = Symtab.extend (selectors, sels),
    1.16 -        updates = Symtab.extend (updates, upds),
    1.17 -        simpset = Simplifier.addsimps (simpset, simps)}
    1.18 -       equalities extinjects extsplit splits extfields fieldext;
    1.19 -  in RecordsData.put data thy end;
    1.20 +fun put_sel_upd names simps = RecordsData.map (fn {records,
    1.21 +  sel_upd = {selectors, updates, simpset},
    1.22 +    equalities, extinjects, extsplit, splits, extfields, fieldext} =>
    1.23 +  make_record_data records
    1.24 +    {selectors = fold (fn name => Symtab.update (name, ())) names selectors,
    1.25 +      updates = fold (fn name => Symtab.update ((suffix updateN) name, name)) names updates,
    1.26 +      simpset = Simplifier.addsimps (simpset, simps)}
    1.27 +      equalities extinjects extsplit splits extfields fieldext);
    1.28  
    1.29  
    1.30  (* access 'equalities' *)