1.1 --- a/src/HOL/Tools/record.ML	Fri Dec 30 15:43:07 2011 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Fri Dec 30 16:43:46 2011 +0100
     1.3 @@ -1645,14 +1645,13 @@
     1.4              asm_simp_tac HOL_ss 1)
     1.5        end);
     1.6  
     1.7 -    val ([induct', inject', surjective', split_meta'], thm_thy) =
     1.8 +    val ([(_, [induct']), (_, [inject']), (_, [surjective']), (_, [split_meta'])], thm_thy) =
     1.9        defs_thy
    1.10 -      |> Global_Theory.add_thms (map (Thm.no_attributes o apfst Binding.name)
    1.11 -           [("ext_induct", induct),
    1.12 -            ("ext_inject", inject),
    1.13 -            ("ext_surjective", surject),
    1.14 -            ("ext_split", split_meta)]);
    1.15 -
    1.16 +      |> Global_Theory.note_thmss ""
    1.17 +          [((Binding.name "ext_induct", []), [([induct], [])]),
    1.18 +           ((Binding.name "ext_inject", []), [([inject], [])]),
    1.19 +           ((Binding.name "ext_surjective", []), [([surject], [])]),
    1.20 +           ((Binding.name "ext_split", []), [([split_meta], [])])];
    1.21    in
    1.22      (((ext_name, ext_type), (ext_tyco, alphas_zeta),
    1.23        extT, induct', inject', surjective', split_meta', ext_def), thm_thy)
    1.24 @@ -2181,39 +2180,37 @@
    1.25        Skip_Proof.prove_global defs_thy [] [] equality_prop
    1.26          (fn _ => asm_full_simp_tac (record_ss addsimps (split_meta :: sel_convs)) 1));
    1.27  
    1.28 -    val ((([sel_convs', upd_convs', sel_defs', upd_defs',
    1.29 -            fold_congs', unfold_congs',
    1.30 -          splits' as [split_meta', split_object', split_ex'], derived_defs'],
    1.31 -          [surjective', equality']),
    1.32 -          [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
    1.33 -      defs_thy
    1.34 -      |> (Global_Theory.add_thmss o map (Thm.no_attributes o apfst Binding.name))
    1.35 -         [("select_convs", sel_convs),
    1.36 -          ("update_convs", upd_convs),
    1.37 -          ("select_defs", sel_defs),
    1.38 -          ("update_defs", upd_defs),
    1.39 -          ("fold_congs", fold_congs),
    1.40 -          ("unfold_congs", unfold_congs),
    1.41 -          ("splits", [split_meta, split_object, split_ex]),
    1.42 -          ("defs", derived_defs)]
    1.43 -      ||>> (Global_Theory.add_thms o map (Thm.no_attributes o apfst Binding.name))
    1.44 -          [("surjective", surjective),
    1.45 -           ("equality", equality)]
    1.46 -      ||>> (Global_Theory.add_thms o (map o apfst o apfst) Binding.name)
    1.47 -        [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
    1.48 -         (("induct", induct), induct_type_global name),
    1.49 -         (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
    1.50 -         (("cases", cases), cases_type_global name)];
    1.51 +    val ([(_, sel_convs'), (_, upd_convs'), (_, sel_defs'), (_, upd_defs'),
    1.52 +          (_, fold_congs'), (_, unfold_congs'),
    1.53 +          (_, splits' as [split_meta', split_object', split_ex']), (_, derived_defs'),
    1.54 +          (_, [surjective']), (_, [equality']), (_, [induct_scheme']), (_, [induct']),
    1.55 +          (_, [cases_scheme']), (_, [cases'])], thms_thy) = defs_thy
    1.56 +      |> Global_Theory.note_thmss ""
    1.57 +       [((Binding.name "select_convs", []), [(sel_convs, [])]),
    1.58 +        ((Binding.name "update_convs", []), [(upd_convs, [])]),
    1.59 +        ((Binding.name "select_defs", []), [(sel_defs, [])]),
    1.60 +        ((Binding.name "update_defs", []), [(upd_defs, [])]),
    1.61 +        ((Binding.name "fold_congs", []), [(fold_congs, [])]),
    1.62 +        ((Binding.name "unfold_congs", []), [(unfold_congs, [])]),
    1.63 +        ((Binding.name "splits", []), [([split_meta, split_object, split_ex], [])]),
    1.64 +        ((Binding.name "defs", []), [(derived_defs, [])]),
    1.65 +        ((Binding.name "surjective", []), [([surjective], [])]),
    1.66 +        ((Binding.name "equality", []), [([equality], [])]),
    1.67 +        ((Binding.name "induct_scheme", induct_type_global (suffix schemeN name)),
    1.68 +          [([induct_scheme], [])]),
    1.69 +        ((Binding.name "induct", induct_type_global name), [([induct], [])]),
    1.70 +        ((Binding.name "cases_scheme", cases_type_global (suffix schemeN name)),
    1.71 +          [([cases_scheme], [])]),
    1.72 +        ((Binding.name "cases", cases_type_global name), [([cases], [])])];
    1.73  
    1.74      val sel_upd_simps = sel_convs' @ upd_convs';
    1.75      val sel_upd_defs = sel_defs' @ upd_defs';
    1.76      val depth = parent_len + 1;
    1.77  
    1.78 -    val ([simps', iffs'], thms_thy') =
    1.79 -      thms_thy
    1.80 -      |> Global_Theory.add_thmss
    1.81 -          [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
    1.82 -           ((Binding.name "iffs", [ext_inject]), [iff_add])];
    1.83 +    val ([(_, simps'), (_, iffs')], thms_thy') = thms_thy
    1.84 +      |> Global_Theory.note_thmss ""
    1.85 +          [((Binding.name "simps", [Simplifier.simp_add]), [(sel_upd_simps, [])]),
    1.86 +           ((Binding.name "iffs", [iff_add]), [([ext_inject], [])])];
    1.87  
    1.88      val info =
    1.89        make_info alphas parent fields extension