diff -r bde4289d793d -r 6d52187fc2a6 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri May 23 16:05:13 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri May 23 16:10:25 2008 +0200
@@ -762,29 +762,16 @@
   the @{text "\<PRINTCODESETUP>"} command.
 
   In some cases, it may be convenient to alter or
-  extend this table;  as an example, we show
-  how to implement finite sets by lists
-  using the conversion @{term [source] "set \<Colon> 'a list \<Rightarrow> 'a set"}
-  as constructor:
-*} (*<*)ML {* nonfix union *} lemmas [code func del] = in_code union_empty1 union_empty2 union_insert Union_code(*>*)
-
-code_datatype set
-
-lemma [code func]: "{} = set []" by simp
+  extend this table;  as an example FIXME
+*}
 
-lemma [code func]: "insert x (set xs) = set (x#xs)" by simp
-
-lemma [code func]: "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
+(* {* code_datatype ... *}
 
-lemma [code func]: "xs \<union> set ys = foldr insert ys xs" by (induct ys) simp_all
+   {* export_code "{}" insert "op \<in>" "op \<union>" "Union" (*<*)in SML(*>*) in SML file "examples/set_list.ML" *}
 
-lemma [code func]: "\<Union>set xs = foldr (op \<union>) xs {}" by (induct xs) simp_all
-
-export_code "{}" insert "op \<in>" "op \<union>" "Union" (*<*)in SML(*>*) in SML file "examples/set_list.ML"
+  {* \lstsml{Thy/examples/set_list.ML} *} *)
 
 text {*
-  \lstsml{Thy/examples/set_list.ML}
-
   \medskip
 
   Changing the representation of existing datatypes requires
@@ -1105,7 +1092,7 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML CodeUnit.read_const: "theory -> string -> string"} \\
-  @{index_ML CodeUnit.head_func: "thm -> string * typ"} \\
+  @{index_ML CodeUnit.head_func: "thm -> string * ((string * sort) list * typ)"} \\
   @{index_ML CodeUnit.rewrite_func: "thm list -> thm -> thm"} \\
   \end{mldecls}