src/HOL/Induct/SList.ML
changeset 5535 678999604ee9
parent 5278 a903b66822e2
child 5977 9f0c8869cf71
     1.1 --- a/src/HOL/Induct/SList.ML	Tue Sep 22 17:08:30 1998 +0200
     1.2 +++ b/src/HOL/Induct/SList.ML	Wed Sep 23 10:03:32 1998 +0200
     1.3 @@ -229,7 +229,7 @@
     1.4  val sexp_ListA_I = A_subset_sexp RS list_subset_sexp RS subsetD;
     1.5  val sexp_A_I = A_subset_sexp RS subsetD;
     1.6  by (rtac (major RS list.induct) 1);
     1.7 -by (ALLGOALS(asm_simp_tac (simpset() addsimps ([sexp_A_I,sexp_ListA_I]@prems))));
     1.8 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [sexp_A_I,sexp_ListA_I]@prems)));
     1.9  qed "List_rec_type";
    1.10  
    1.11  (** Generalized map functionals **)