src/HOL/Bali/Basis.thy
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 16121 a80aa66d2271
     1.1 --- a/src/HOL/Bali/Basis.thy	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -188,7 +188,7 @@
     1.4  (*###to be phased out *)
     1.5  ML {* 
     1.6  fun noAll_simpset () = simpset() setmksimps 
     1.7 -	mksimps (filter (fn (x,_) => x<>"All") mksimps_pairs)
     1.8 +	mksimps (List.filter (fn (x,_) => x<>"All") mksimps_pairs)
     1.9  *}
    1.10  
    1.11  lemma All_Ex_refl_eq2 [simp]: