--- 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,
--- 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;