# HG changeset patch
# User haftmann
# Date 1242282126 -7200
# Node ID 2ce5c0c4d69728bfe64712ff34c7bd15c213f2d7
# Parent  8f609d1e7002085123d0be06fd255392c5dc97ab
adapted code tutorial to recent changes in code

diff -r 8f609d1e7002 -r 2ce5c0c4d697 doc-src/Codegen/Thy/ML.thy
--- a/doc-src/Codegen/Thy/ML.thy	Wed May 13 21:22:48 2009 +0200
+++ b/doc-src/Codegen/Thy/ML.thy	Thu May 14 08:22:06 2009 +0200
@@ -25,11 +25,11 @@
   @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
   @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
   @{index_ML Code.add_eqnl: "string * (thm * bool) list lazy -> theory -> theory"} \\
-  @{index_ML Code.map_pre: "(simpset -> simpset) -> theory -> theory"} \\
-  @{index_ML Code.map_post: "(simpset -> simpset) -> theory -> theory"} \\
-  @{index_ML Code.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
+  @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\
+  @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\
+  @{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
     -> theory -> theory"} \\
-  @{index_ML Code.del_functrans: "string -> 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
     -> (string * sort) list * (string * typ list) list"} \\
@@ -48,10 +48,10 @@
      suspended code equations @{text lthms} for constant
      @{text const} to executable content.
 
-  \item @{ML Code.map_pre}~@{text "f"}~@{text "thy"} changes
+  \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes
      the preprocessor simpset.
 
-  \item @{ML Code.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
+  \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
      function transformer @{text f} (named @{text name}) to executable content;
      @{text f} is a transformer of the code equations belonging
      to a certain function definition, depending on the
@@ -59,7 +59,7 @@
      transformation took place;  otherwise, the whole process will be iterated
      with the new code equations.
 
-  \item @{ML Code.del_functrans}~@{text "name"}~@{text "thy"} removes
+  \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes
      function transformer named @{text name} from executable content.
 
   \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
@@ -79,7 +79,6 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML Code_Unit.read_const: "theory -> string -> string"} \\
-  @{index_ML Code_Unit.head_eqn: "theory -> thm -> string * ((string * sort) list * typ)"} \\
   @{index_ML Code_Unit.rewrite_eqn: "simpset -> thm -> thm"} \\
   \end{mldecls}
 
@@ -88,9 +87,6 @@
   \item @{ML Code_Unit.read_const}~@{text thy}~@{text s}
      reads a constant as a concrete term expression @{text s}.
 
-  \item @{ML Code_Unit.head_eqn}~@{text thy}~@{text thm}
-     extracts the constant and its type from a code equation @{text thm}.
-
   \item @{ML Code_Unit.rewrite_eqn}~@{text ss}~@{text thm}
      rewrites a code equation @{text thm} with a simpset @{text ss};
      only arguments and right hand side are rewritten,
diff -r 8f609d1e7002 -r 2ce5c0c4d697 doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Wed May 13 21:22:48 2009 +0200
+++ b/doc-src/more_antiquote.ML	Thu May 14 08:22:06 2009 +0200
@@ -88,9 +88,9 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val const = Code_Unit.check_const thy raw_const;
-    val (_, funcgr) = Code_Wellsorted.obtain thy [const] [];
+    val (_, funcgr) = Code_Preproc.obtain thy [const] [];
     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
-    val thms = Code_Wellsorted.eqns funcgr const
+    val thms = Code_Preproc.eqns funcgr const
       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
       |> map (holize o no_vars ctxt o AxClass.overload thy);
   in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end;