diff -r 92d8ff6af82c -r 90fed3d4430f doc-src/Codegen/Thy/ML.thy --- a/doc-src/Codegen/Thy/ML.thy Thu May 14 15:09:47 2009 +0200 +++ b/doc-src/Codegen/Thy/ML.thy Thu May 14 15:09:48 2009 +0200 @@ -78,16 +78,16 @@ text %mlref {* \begin{mldecls} - @{index_ML Code_Unit.read_const: "theory -> string -> string"} \\ - @{index_ML Code_Unit.rewrite_eqn: "simpset -> thm -> thm"} \\ + @{index_ML Code.read_const: "theory -> string -> string"} \\ + @{index_ML Code.rewrite_eqn: "simpset -> thm -> thm"} \\ \end{mldecls} \begin{description} - \item @{ML Code_Unit.read_const}~@{text thy}~@{text s} + \item @{ML Code.read_const}~@{text thy}~@{text s} reads a constant as a concrete term expression @{text s}. - \item @{ML Code_Unit.rewrite_eqn}~@{text ss}~@{text thm} + \item @{ML Code.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, not the head of the code equation.