diff -r 165cd386288d -r 1b09880d9734 doc-src/Codegen/Thy/examples/example.ML
--- a/doc-src/Codegen/Thy/examples/example.ML	Tue Jun 29 07:55:18 2010 +0200
+++ b/doc-src/Codegen/Thy/examples/example.ML	Tue Jun 29 11:25:03 2010 +0200
@@ -1,7 +1,6 @@
 structure Example : sig
   val foldl : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
   val rev : 'a list -> 'a list
-  val list_case : 'a -> ('b -> 'b list -> 'a) -> 'b list -> 'a
   datatype 'a queue = AQueue of 'a list * 'a list
   val empty : 'a queue
   val dequeue : 'a queue -> 'a option * 'a queue
@@ -13,9 +12,6 @@
 
 fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;
 
-fun list_case f1 f2 (a :: lista) = f2 a lista
-  | list_case f1 f2 [] = f1;
-
 datatype 'a queue = AQueue of 'a list * 'a list;
 
 val empty : 'a queue = AQueue ([], []);