src/HOL/ex/Term.ML

 by (REPEAT (ares_tac prems 1));
 qed "Term_induct2";
 
 (*** Structural Induction on the abstract type 'a term ***)
 
-val list_all_ss = map_ss addsimps [list_all_Nil, list_all_Cons];
-
 val Rep_term_in_sexp =
     Rep_term RS (range_Leaf_subset_sexp RS term_subset_sexp RS subsetD);
 
 (*Induction for the abstract type 'a term*)
 val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def]

 by (stac Abs_map_CONS 2);
 by (etac conjunct1 2);
 by (etac rev_subsetD 2);
 by (rtac list_subset_sexp 2);
 by (fast_tac set_cs 2);
-by (ALLGOALS (asm_simp_tac list_all_ss));
+by (ALLGOALS Asm_simp_tac);
 qed "term_induct";
 
 (*Induction for the abstract type 'a term*)
 val prems = goal Term.thy 
     "[| !!x. R(App x Nil);  \
 \       !!x t ts. R(App x ts) ==> R(App x (t#ts))  \
 \    |] ==> R(t)";
 by (rtac term_induct 1);  (*types force good instantiation*)
 by (etac rev_mp 1);
-by (rtac list_induct 1);  (*types force good instantiation*)
-by (ALLGOALS (asm_simp_tac (list_all_ss addsimps prems)));
+by (rtac list_induct2 1);  (*types force good instantiation*)
+by (ALLGOALS (asm_simp_tac (!simpset addsimps prems)));
 qed "term_induct2";
 
 (*Perform induction on xs. *)
 fun term_ind2_tac a i = 
     EVERY [res_inst_tac [("t",a)] term_induct2 i,

     "N: list(term(A)) ==>  \
 \    !M. (N,M): pred_sexp^+ --> \
 \        Abs_map (cut h (pred_sexp^+) M) N = \
 \        Abs_map h N";
 by (rtac (prem RS list.induct) 1);
-by (simp_tac list_all_ss 1);
+by (Simp_tac 1);
 by (strip_tac 1);
 by (etac (pred_sexp_CONS_D RS conjE) 1);
-by (asm_simp_tac (list_all_ss addsimps [trancl_pred_sexpD1, cut_apply]) 1);
+by (asm_simp_tac (!simpset addsimps [trancl_pred_sexpD1]) 1);
 qed "Abs_map_lemma";
 
 val [prem1,prem2,A_subset_sexp] = goal Term.thy
     "[| M: sexp;  N: list(term(A));  A<=sexp |] ==> \
 \    Term_rec (M$N) d = d M N (Abs_map (%Z. Term_rec Z d) N)";
 by (rtac (Term_rec_unfold RS trans) 1);
 by (simp_tac (HOL_ss addsimps
       [Split,
        prem2 RS Abs_map_lemma RS spec RS mp, pred_sexpI2 RS r_into_trancl,
        prem1, prem2 RS rev_subsetD, list_subset_sexp,
-       term_subset_sexp, A_subset_sexp])1);
+       term_subset_sexp, A_subset_sexp]) 1);
 qed "Term_rec";
 
 (*** term_rec -- by Term_rec ***)
 
 local

   val Rep_Tlist = Rep_term RS Rep_map_type1;
   val Rep_Term_rec = range_Leaf_subset_sexp RSN (2,Rep_Tlist RSN(2,Term_rec));
 
   (*Now avoids conditional rewriting with the premise N: list(term(A)),
     since A will be uninstantiated and will cause rewriting to fail. *)
-  val term_rec_ss = HOL_ss 
+  val term_rec_ss = HOL_ss
       addsimps [Rep_Tlist RS (rangeI RS term.APP_I RS Abs_term_inverse),  
-	       Rep_term_in_sexp, Rep_Term_rec, Rep_term_inverse,
-	       inj_Leaf, Inv_f_f,
-	       Abs_Rep_map, map_ident, sexp.LeafI]
+                Rep_term_in_sexp, Rep_Term_rec, Rep_term_inverse, inj_Leaf,
+                Inv_f_f, Abs_Rep_map, map_ident2, sexp.LeafI]
 in
 
 val term_rec = prove_goalw Term.thy
 	 [term_rec_def, App_def, Rep_Tlist_def, Abs_Tlist_def]
     "term_rec (App f ts) d = d f ts (map (%t. term_rec t d) ts)"