1.1 --- a/doc-src/Codegen/Thy/ML.thy	Wed May 13 21:22:48 2009 +0200
     1.2 +++ b/doc-src/Codegen/Thy/ML.thy	Thu May 14 08:22:06 2009 +0200
     1.3 @@ -25,11 +25,11 @@
     1.4    @{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
     1.5    @{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
     1.6    @{index_ML Code.add_eqnl: "string * (thm * bool) list lazy -> theory -> theory"} \\
     1.7 -  @{index_ML Code.map_pre: "(simpset -> simpset) -> theory -> theory"} \\
     1.8 -  @{index_ML Code.map_post: "(simpset -> simpset) -> theory -> theory"} \\
     1.9 -  @{index_ML Code.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
    1.10 +  @{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\
    1.11 +  @{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\
    1.12 +  @{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
    1.13      -> theory -> theory"} \\
    1.14 -  @{index_ML Code.del_functrans: "string -> theory -> theory"} \\
    1.15 +  @{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
    1.16    @{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
    1.17    @{index_ML Code.get_datatype: "theory -> string
    1.18      -> (string * sort) list * (string * typ list) list"} \\
    1.19 @@ -48,10 +48,10 @@
    1.20       suspended code equations @{text lthms} for constant
    1.21       @{text const} to executable content.
    1.22  
    1.23 -  \item @{ML Code.map_pre}~@{text "f"}~@{text "thy"} changes
    1.24 +  \item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes
    1.25       the preprocessor simpset.
    1.26  
    1.27 -  \item @{ML Code.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
    1.28 +  \item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds
    1.29       function transformer @{text f} (named @{text name}) to executable content;
    1.30       @{text f} is a transformer of the code equations belonging
    1.31       to a certain function definition, depending on the
    1.32 @@ -59,7 +59,7 @@
    1.33       transformation took place;  otherwise, the whole process will be iterated
    1.34       with the new code equations.
    1.35  
    1.36 -  \item @{ML Code.del_functrans}~@{text "name"}~@{text "thy"} removes
    1.37 +  \item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes
    1.38       function transformer named @{text name} from executable content.
    1.39  
    1.40    \item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds
    1.41 @@ -79,7 +79,6 @@
    1.42  text %mlref {*
    1.43    \begin{mldecls}
    1.44    @{index_ML Code_Unit.read_const: "theory -> string -> string"} \\
    1.45 -  @{index_ML Code_Unit.head_eqn: "theory -> thm -> string * ((string * sort) list * typ)"} \\
    1.46    @{index_ML Code_Unit.rewrite_eqn: "simpset -> thm -> thm"} \\
    1.47    \end{mldecls}
    1.48  
    1.49 @@ -88,9 +87,6 @@
    1.50    \item @{ML Code_Unit.read_const}~@{text thy}~@{text s}
    1.51       reads a constant as a concrete term expression @{text s}.
    1.52  
    1.53 -  \item @{ML Code_Unit.head_eqn}~@{text thy}~@{text thm}
    1.54 -     extracts the constant and its type from a code equation @{text thm}.
    1.55 -
    1.56    \item @{ML Code_Unit.rewrite_eqn}~@{text ss}~@{text thm}
    1.57       rewrites a code equation @{text thm} with a simpset @{text ss};
    1.58       only arguments and right hand side are rewritten,

     2.1 --- a/doc-src/more_antiquote.ML	Wed May 13 21:22:48 2009 +0200
     2.2 +++ b/doc-src/more_antiquote.ML	Thu May 14 08:22:06 2009 +0200
     2.3 @@ -88,9 +88,9 @@
     2.4    let
     2.5      val thy = ProofContext.theory_of ctxt;
     2.6      val const = Code_Unit.check_const thy raw_const;
     2.7 -    val (_, funcgr) = Code_Wellsorted.obtain thy [const] [];
     2.8 +    val (_, funcgr) = Code_Preproc.obtain thy [const] [];
     2.9      fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
    2.10 -    val thms = Code_Wellsorted.eqns funcgr const
    2.11 +    val thms = Code_Preproc.eqns funcgr const
    2.12        |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    2.13        |> map (holize o no_vars ctxt o AxClass.overload thy);
    2.14    in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end;