# HG changeset patch
# User haftmann
# Date 1275319766 -7200
# Node ID 1f1f9cbd23ae39520cbf9079a3edc0416c1510d4
# Parent  c40c9b05952c0e276da2bb4a2486046ce79b86ec
adjusted

diff -r c40c9b05952c -r 1f1f9cbd23ae doc-src/Codegen/Thy/Further.thy
--- a/doc-src/Codegen/Thy/Further.thy	Mon May 31 10:29:04 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy	Mon May 31 17:29:26 2010 +0200
@@ -94,7 +94,7 @@
   whole @{text SML} is read, the necessary code is generated transparently
   and the corresponding constant names are inserted.  This technique also
   allows to use pattern matching on constructors stemming from compiled
-  @{text datatypes}.
+  @{text "datatypes"}.
 
   For a less simplistic example, theory @{theory Ferrack} is
   a good reference.
diff -r c40c9b05952c -r 1f1f9cbd23ae doc-src/Codegen/Thy/ML.thy
--- a/doc-src/Codegen/Thy/ML.thy	Mon May 31 10:29:04 2010 +0200
+++ b/doc-src/Codegen/Thy/ML.thy	Mon May 31 17:29:26 2010 +0200
@@ -30,9 +30,9 @@
     -> theory -> theory"} \\
   @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
   @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
-  @{index_ML Code.get_datatype: "theory -> string
+  @{index_ML Code.get_type: "theory -> string
     -> (string * sort) list * (string * typ list) list"} \\
-  @{index_ML Code.get_datatype_of_constr: "theory -> string -> string option"}
+  @{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"}
   \end{mldecls}
 
   \begin{description}
@@ -61,7 +61,7 @@
      a datatype to executable content, with generation
      set @{text cs}.
 
-  \item @{ML Code.get_datatype_of_constr}~@{text "thy"}~@{text "const"}
+  \item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"}
      returns type constructor corresponding to
      constructor @{text const}; returns @{text NONE}
      if @{text const} is no constructor.
@@ -105,7 +105,7 @@
   merge, which is a little bit nasty from an implementation
   point of view.  The framework provides a solution
   to this technical challenge by providing a functorial
-  data slot @{ML_functor CodeDataFun}; on instantiation
+  data slot @{ML_functor Code_Data}; on instantiation
   of this functor, the following types and operations
   are required:
 
@@ -131,7 +131,7 @@
 
   \end{description}
 
-  \noindent An instance of @{ML_functor CodeDataFun} provides the following
+  \noindent An instance of @{ML_functor Code_Data} provides the following
   interface:
 
   \medskip