diff -r fdd37cfcd4a3 -r 27a61a3266d8 src/HOL/ex/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Mon Mar 14 12:34:08 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Mon Mar 14 12:34:09 2011 +0100
@@ -115,12 +115,12 @@
                  
 subsection {* Necessary instantiation for quickcheck generator *}
 
-instantiation tree :: (serial) serial
+instantiation tree :: (narrowing) narrowing
 begin
 
-function series_tree
+function narrowing_tree
 where
-  "series_tree d = sum (cons ET) (apply (apply (apply (apply (cons MKT) series) series_tree) series_tree) series) d"
+  "narrowing_tree d = sum (cons ET) (apply (apply (apply (apply (cons MKT) narrowing) narrowing_tree) narrowing_tree) narrowing) d"
 by pat_completeness auto
 
 termination proof (relation "measure nat_of")