1.1 --- a/src/HOL/Tools/record.ML	Sun Jan 15 13:55:01 2012 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sun Jan 15 14:00:07 2012 +0100
     1.3 @@ -379,9 +379,7 @@
     1.4     {selectors: (int * bool) Symtab.table,
     1.5      updates: string Symtab.table,
     1.6      simpset: simpset,
     1.7 -    defset: simpset,
     1.8 -    foldcong: simpset,
     1.9 -    unfoldcong: simpset},
    1.10 +    defset: simpset},
    1.11    equalities: thm Symtab.table,
    1.12    extinjects: thm list,
    1.13    extsplit: thm Symtab.table,  (*maps extension name to split rule*)
    1.14 @@ -401,16 +399,12 @@
    1.15    val empty =
    1.16      make_data Symtab.empty
    1.17        {selectors = Symtab.empty, updates = Symtab.empty,
    1.18 -          simpset = HOL_basic_ss, defset = HOL_basic_ss,
    1.19 -          foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
    1.20 +        simpset = HOL_basic_ss, defset = HOL_basic_ss}
    1.21         Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
    1.22    val extend = I;
    1.23    fun merge
    1.24     ({records = recs1,
    1.25 -     sel_upd =
    1.26 -      {selectors = sels1, updates = upds1,
    1.27 -       simpset = ss1, defset = ds1,
    1.28 -       foldcong = fc1, unfoldcong = uc1},
    1.29 +     sel_upd = {selectors = sels1, updates = upds1, simpset = ss1, defset = ds1},
    1.30       equalities = equalities1,
    1.31       extinjects = extinjects1,
    1.32       extsplit = extsplit1,
    1.33 @@ -418,10 +412,7 @@
    1.34       extfields = extfields1,
    1.35       fieldext = fieldext1},
    1.36      {records = recs2,
    1.37 -     sel_upd =
    1.38 -      {selectors = sels2, updates = upds2,
    1.39 -       simpset = ss2, defset = ds2,
    1.40 -       foldcong = fc2, unfoldcong = uc2},
    1.41 +     sel_upd = {selectors = sels2, updates = upds2, simpset = ss2, defset = ds2},
    1.42       equalities = equalities2,
    1.43       extinjects = extinjects2,
    1.44       extsplit = extsplit2,
    1.45 @@ -433,9 +424,7 @@
    1.46        {selectors = Symtab.merge (K true) (sels1, sels2),
    1.47          updates = Symtab.merge (K true) (upds1, upds2),
    1.48          simpset = Simplifier.merge_ss (ss1, ss2),
    1.49 -        defset = Simplifier.merge_ss (ds1, ds2),
    1.50 -        foldcong = Simplifier.merge_ss (fc1, fc2),
    1.51 -        unfoldcong = Simplifier.merge_ss (uc1, uc2)}
    1.52 +        defset = Simplifier.merge_ss (ds1, ds2)}
    1.53        (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
    1.54        (Thm.merge_thms (extinjects1, extinjects2))
    1.55        (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
    1.56 @@ -482,22 +471,21 @@
    1.57      | NONE => NONE)
    1.58    end;
    1.59  
    1.60 -fun put_sel_upd names more depth simps defs (folds, unfolds) thy =
    1.61 +fun put_sel_upd names more depth simps defs thy =
    1.62    let
    1.63      val all = names @ [more];
    1.64      val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
    1.65      val upds = map (suffix updateN) all ~~ all;
    1.66  
    1.67 -    val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
    1.68 +    val {records, sel_upd = {selectors, updates, simpset, defset},
    1.69        equalities, extinjects, extsplit, splits, extfields, fieldext} = Data.get thy;
    1.70 -    val data = make_data records
    1.71 -      {selectors = fold Symtab.update_new sels selectors,
    1.72 -        updates = fold Symtab.update_new upds updates,
    1.73 -        simpset = simpset addsimps simps,
    1.74 -        defset = defset addsimps defs,
    1.75 -        foldcong = foldcong |> fold Simplifier.add_cong folds,
    1.76 -        unfoldcong = unfoldcong |> fold Simplifier.add_cong unfolds}
    1.77 -       equalities extinjects extsplit splits extfields fieldext;
    1.78 +    val data =
    1.79 +      make_data records
    1.80 +        {selectors = fold Symtab.update_new sels selectors,
    1.81 +          updates = fold Symtab.update_new upds updates,
    1.82 +          simpset = simpset addsimps simps,
    1.83 +          defset = defset addsimps defs}
    1.84 +         equalities extinjects extsplit splits extfields fieldext;
    1.85    in Data.put data thy end;
    1.86  
    1.87  
    1.88 @@ -2214,7 +2202,7 @@
    1.89      val final_thy =
    1.90        thms_thy'
    1.91        |> put_record name info
    1.92 -      |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')
    1.93 +      |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs
    1.94        |> add_equalities extension_id equality'
    1.95        |> add_extinjects ext_inject
    1.96        |> add_extsplit extension_name ext_split