1.1 --- a/src/HOL/Tools/record.ML	Fri Dec 30 14:19:58 2011 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Fri Dec 30 15:43:07 2011 +0100
     1.3 @@ -2091,8 +2091,8 @@
     1.4  
     1.5      (* 3rd stage: thms_thy *)
     1.6  
     1.7 -    val ss = get_simpset defs_thy;
     1.8 -    val sel_upd_ss = ss addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms);
     1.9 +    val record_ss = get_simpset defs_thy;
    1.10 +    val sel_upd_ss = record_ss addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms);
    1.11  
    1.12      val (sel_convs, upd_convs) =
    1.13        timeit_msg ctxt "record sel_convs/upd_convs proof:" (fn () =>
    1.14 @@ -2177,22 +2177,9 @@
    1.15                  @{thms not_not Not_eq_iff})) 1 THEN
    1.16            rtac split_object 1));
    1.17  
    1.18 -    fun equality_tac thms =
    1.19 -      let
    1.20 -        val s' :: s :: eqs = rev thms;
    1.21 -        val ss' = ss addsimps (s' :: s :: sel_convs);
    1.22 -        val eqs' = map (simplify ss') eqs;
    1.23 -      in simp_tac (HOL_basic_ss addsimps (s' :: s :: eqs')) 1 end;
    1.24 -
    1.25      val equality = timeit_msg ctxt "record equality proof:" (fn () =>
    1.26 -      Skip_Proof.prove_global defs_thy [] [] equality_prop (fn {context, ...} =>
    1.27 -        fn st =>
    1.28 -          let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
    1.29 -            st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 THEN
    1.30 -              res_inst_tac context [((rN, 0), s')] cases_scheme 1 THEN
    1.31 -              Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1)
    1.32 -             (*asm_full_simp_tac sel_upd_ss would also work but is less efficient*)
    1.33 -          end));
    1.34 +      Skip_Proof.prove_global defs_thy [] [] equality_prop
    1.35 +        (fn _ => asm_full_simp_tac (record_ss addsimps (split_meta :: sel_convs)) 1));
    1.36  
    1.37      val ((([sel_convs', upd_convs', sel_defs', upd_defs',
    1.38              fold_congs', unfold_congs',