filter_size -> length_filter

--- a/src/HOL/ex/Recdef.thy	Fri Feb 06 18:55:18 1998 +0100
+++ b/src/HOL/ex/Recdef.thy	Fri Feb 06 18:55:57 1998 +0100
@@ -31,7 +31,7 @@
 
 consts qsort   ::"('a => 'a => bool) * 'a list => 'a list"
 recdef qsort "measure (size o snd)"
-    simpset "simpset() addsimps [le_eq_less_Suc RS sym, filter_size]"
+    simpset "simpset() addsimps [le_eq_less_Suc RS sym, length_filter]"
     "qsort(ord, [])    = []"
     "qsort(ord, x#rst) = qsort(ord, filter(Not o ord x) rst)  
                          @ [x] @