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