# HG changeset patch
# User nipkow
# Date 886787757 -3600
# Node ID 73227403d497aafacee25a954c40279ca53e5ece
# Parent  579e0ef2df6bbc545a221e381f89c101124d02e1
filter_size -> length_filter

diff -r 579e0ef2df6b -r 73227403d497 src/HOL/ex/Recdef.thy
--- 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] @