# HG changeset patch
# User haftmann
# Date 1211551825 -7200
# Node ID 6d52187fc2a64a6edcfcba42f1ece68d2827d592
# Parent  bde4289d793dd5820a893be3846c765c729efff1
temporary adjustment

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}
 
diff -r bde4289d793d -r 6d52187fc2a6 doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Fri May 23 16:05:13 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Fri May 23 16:10:25 2008 +0200
@@ -993,120 +993,12 @@
   the \isa{{\isasymPRINTCODESETUP}} 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 \isa{{\isachardoublequote}set\ {\isasymColon}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequote}}
-  as constructor:%
+  extend this table;  as an example FIXME%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ %
-\isadelimML
 %
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-\isanewline
-\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
-\ set\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}\ {\isacharequal}\ set\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ simp%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}insert\ x\ {\isacharparenleft}set\ xs{\isacharparenright}\ {\isacharequal}\ set\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}{\isachardoublequoteclose}%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ simp%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymunion}\ set\ ys\ {\isacharequal}\ foldr\ insert\ ys\ xs{\isachardoublequoteclose}%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ ys{\isacharparenright}\ simp{\isacharunderscore}all%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymUnion}set\ xs\ {\isacharequal}\ foldr\ {\isacharparenleft}op\ {\isasymunion}{\isacharparenright}\ xs\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\isanewline
-\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ insert\ {\isachardoublequoteopen}op\ {\isasymin}{\isachardoublequoteclose}\ {\isachardoublequoteopen}op\ {\isasymunion}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Union{\isachardoublequoteclose}\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}set{\isacharunderscore}list{\isachardot}ML{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
-\lstsml{Thy/examples/set_list.ML}
-
-  \medskip
+\medskip
 
   Changing the representation of existing datatypes requires
   some care with respect to pattern matching and such.%
@@ -1565,7 +1457,7 @@
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexml{CodeUnit.read\_const}\verb|CodeUnit.read_const: theory -> string -> string| \\
-  \indexml{CodeUnit.head\_func}\verb|CodeUnit.head_func: thm -> string * typ| \\
+  \indexml{CodeUnit.head\_func}\verb|CodeUnit.head_func: thm -> string * ((string * sort) list * typ)| \\
   \indexml{CodeUnit.rewrite\_func}\verb|CodeUnit.rewrite_func: thm list -> thm -> thm| \\
   \end{mldecls}