# HG changeset patch
# User haftmann
# Date 1282047552 -7200
# Node ID 628fee3eb449222ea9d1502b10d1fa96557e8032
# Parent  cfe74b0eecb123e7e26392b69bd614417499dcb4
nicer code for rev

diff -r cfe74b0eecb1 -r 628fee3eb449 doc-src/Codegen/Thy/Setup.thy
--- a/doc-src/Codegen/Thy/Setup.thy	Tue Aug 17 14:19:12 2010 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy	Tue Aug 17 14:19:12 2010 +0200
@@ -1,5 +1,5 @@
 theory Setup
-imports Complex_Main
+imports Complex_Main More_List
 uses
   "../../antiquote_setup.ML"
   "../../more_antiquote.ML"
diff -r cfe74b0eecb1 -r 628fee3eb449 doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Tue Aug 17 14:19:12 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Tue Aug 17 14:19:12 2010 +0200
@@ -141,7 +141,8 @@
 \isatypewriter%
 \noindent%
 \hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val id :~'a -> 'a\\
+\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
 \hspace*{0pt} ~val rev :~'a list -> 'a list\\
 \hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
 \hspace*{0pt} ~val empty :~'a queue\\
@@ -149,10 +150,12 @@
 \hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
 \hspace*{0pt}end = struct\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun foldl f a [] = a\\
-\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
+\hspace*{0pt}fun id x = (fn xa => xa) x;\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}fun fold f [] = id\\
+\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
 \hspace*{0pt}\\
 \hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
 \hspace*{0pt}\\
diff -r cfe74b0eecb1 -r 628fee3eb449 doc-src/Codegen/Thy/examples/example.ML
--- a/doc-src/Codegen/Thy/examples/example.ML	Tue Aug 17 14:19:12 2010 +0200
+++ b/doc-src/Codegen/Thy/examples/example.ML	Tue Aug 17 14:19:12 2010 +0200
@@ -1,5 +1,6 @@
 structure Example : sig
-  val foldl : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
+  val id : 'a -> 'a
+  val fold : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val rev : 'a list -> 'a list
   datatype 'a queue = AQueue of 'a list * 'a list
   val empty : 'a queue
@@ -7,10 +8,12 @@
   val enqueue : 'a -> 'a queue -> 'a queue
 end = struct
 
-fun foldl f a [] = a
-  | foldl f a (x :: xs) = foldl f (f a x) xs;
+fun id x = (fn xa => xa) x;
 
-fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;
+fun fold f [] = id
+  | fold f (x :: xs) = fold f xs o f x;
+
+fun rev xs = fold (fn a => fn b => a :: b) xs [];
 
 datatype 'a queue = AQueue of 'a list * 'a list;