src/HOL/Tools/record.ML

 type data =
  {records: info Symtab.table,
   sel_upd:
    {selectors: (int * bool) Symtab.table,
     updates: string Symtab.table,
-    simpset: Simplifier.simpset,
-    defset: Simplifier.simpset,
-    foldcong: Simplifier.simpset,
-    unfoldcong: Simplifier.simpset},
+    simpset: simpset,
+    defset: simpset,
+    foldcong: simpset,
+    unfoldcong: simpset},
   equalities: thm Symtab.table,
   extinjects: thm list,
   extsplit: thm Symtab.table,  (*maps extension name to split rule*)
   splits: (thm * thm * thm * thm) Symtab.table,  (*!!, ALL, EX - split-equalities, induct rule*)
   extfields: (string * typ) list Symtab.table,  (*maps extension to its fields*)

     val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
       equalities, extinjects, extsplit, splits, extfields, fieldext} = Data.get thy;
     val data = make_data records
       {selectors = fold Symtab.update_new sels selectors,
         updates = fold Symtab.update_new upds updates,
-        simpset = Simplifier.addsimps (simpset, simps),
-        defset = Simplifier.addsimps (defset, defs),
+        simpset = simpset addsimps simps,
+        defset = defset addsimps defs,
         foldcong = foldcong |> fold Simplifier.add_cong folds,
         unfoldcong = unfoldcong |> fold Simplifier.add_cong unfolds}
        equalities extinjects extsplit splits extfields fieldext;
   in Data.put data thy end;
 

 
     val simprocs = if has_rec goal then [split_simproc P] else [];
     val thms' = @{thms o_apply K_record_comp} @ thms;
   in
     EVERY split_frees_tacs THEN
-    Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i
+    full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i
   end);
 
 
 (* split_tac *)
 

     fun is_all (Const (@{const_name all}, _) $ _) = ~1
       | is_all (Const (@{const_name All}, _) $ _) = ~1
       | is_all _ = 0;
   in
     if has_rec goal then
-      Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [split_simproc is_all]) i
+      full_simp_tac (HOL_basic_ss addsimprocs [split_simproc is_all]) i
     else no_tac
   end);
 
 
 (* wrapper *)

 fun induct_type_global name = [case_names_fields, Induct.induct_type name];
 fun cases_type_global name = [case_names_fields, Induct.cases_type name];
 
 
 (* tactics *)
-
-fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
 
 (*Do case analysis / induction according to rule on last parameter of ith subgoal
   (or on s if there are no parameters).
   Instatiation of record variable (and predicate) in rule is calculated to
   avoid problems with higher order unification.*)

       (HOLogic.mk_Trueprop o HOLogic.mk_eq)
         (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
          Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT));
     fun tac eq_def =
       Class.intro_classes_tac []
-      THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def])
+      THEN rewrite_goals_tac [Simpdata.mk_eq eq_def]
       THEN ALLGOALS (rtac @{thm refl});
-    fun mk_eq thy eq_def = Simplifier.rewrite_rule
-      [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject;
+    fun mk_eq thy eq_def =
+      Simplifier.rewrite_rule
+        [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject;
     fun mk_eq_refl thy =
       @{thm equal_refl}
       |> Thm.instantiate
         ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
       |> AxClass.unoverload thy;

 
     (* 3rd stage: thms_thy *)
 
     val prove = Skip_Proof.prove_global defs_thy;
 
-    fun prove_simp ss simps =
-      let val tac = simp_all_tac ss simps
-      in fn prop => prove [] [] prop (K tac) end;
-
     val ss = get_simpset defs_thy;
+    val simp_defs_tac =
+      asm_full_simp_tac (ss addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms));
 
     val sel_convs = timeit_msg ctxt "record sel_convs proof:" (fn () =>
-      map (prove_simp ss (sel_defs @ accessor_thms)) sel_conv_props);
+      map (fn prop => prove [] [] prop (K (ALLGOALS simp_defs_tac))) sel_conv_props);
 
     val upd_convs = timeit_msg ctxt "record upd_convs proof:" (fn () =>
-      map (prove_simp ss (upd_defs @ updator_thms)) upd_conv_props);
+      map (fn prop => prove [] [] prop (K (ALLGOALS simp_defs_tac))) upd_conv_props);
 
     val (fold_congs, unfold_congs) = timeit_msg ctxt "record upd fold/unfold congs:" (fn () =>
       let
         val symdefs = map Thm.symmetric (sel_defs @ upd_defs);
         val fold_ss = HOL_basic_ss addsimps symdefs;

 
     val cases = timeit_msg ctxt "record cases proof:" (fn () =>
       prove [] [] cases_prop
         (fn _ =>
           try_param_tac rN cases_scheme 1 THEN
-          simp_all_tac HOL_basic_ss [@{thm unit_all_eq1}]));
+          ALLGOALS (asm_full_simp_tac (HOL_basic_ss addsimps [@{thm unit_all_eq1}]))));
 
     val surjective = timeit_msg ctxt "record surjective proof:" (fn () =>
       let
         val leaf_ss =
           get_sel_upd_defs defs_thy addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id});

         fn st =>
           let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
             st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 THEN
               res_inst_tac context [((rN, 0), s')] cases_scheme 1 THEN
               Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1)
-             (*simp_all_tac ss (sel_convs) would also work but is less efficient*)
+             (*simp_defs_tac would also work but is less efficient*)
           end));
 
     val ((([sel_convs', upd_convs', sel_defs', upd_defs',
             fold_congs', unfold_congs',
           splits' as [split_meta', split_object', split_ex'], derived_defs'],