# HG changeset patch
# User wenzelm
# Date 1194701478 -3600
# Node ID 5200374fda5d9e66075b1a0ee316b3e931f8cd8f
# Parent  f12613fda79d3afec9346c98d10a1f958b22ed63
replaced @{const} (allows name only) by proper @{term};

diff -r f12613fda79d -r 5200374fda5d doc-src/IsarAdvanced/Classes/Thy/Classes.thy
--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Fri Nov 09 23:24:31 2007 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Sat Nov 10 14:31:18 2007 +0100
@@ -412,7 +412,7 @@
   a canonical interpretation as type classes.
   Anyway, there is also the possibility of other interpretations.
   For example, also @{text "list"}s form a monoid with
-  @{const "op @"} and @{const "[]"} as operations, but it
+  @{term "op @"} and @{term "[]"} as operations, but it
   seems inappropriate to apply to lists
   the same operations as for genuinly algebraic types.
   In such a case, we simply can do a particular interpretation
diff -r f12613fda79d -r 5200374fda5d doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Nov 09 23:24:31 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Sat Nov 10 14:31:18 2007 +0100
@@ -471,7 +471,7 @@
        @{text "Code_Integer"}.
     \item[@{text "Efficient_Nat"}] \label{eff_nat} implements natural numbers by integers,
        which in general will result in higher efficency; pattern
-       matching with @{const "0\<Colon>nat"} / @{const "Suc"}
+       matching with @{term "0\<Colon>nat"} / @{const "Suc"}
        is eliminated;  includes @{text "Code_Integer"}.
     \item[@{text "Code_Index"}] provides an additional datatype
        @{text index} which is mapped to target-language built-in integers.
@@ -548,13 +548,13 @@
   theorems written in ML -- rewrite rules are generated dependent
   on the function theorems for a certain function.  One
   application is the implicit expanding of @{typ nat} numerals
-  to @{const "0\<Colon>nat"} / @{const Suc} representation.  See further
+  to @{term "0\<Colon>nat"} / @{const Suc} representation.  See further
   \secref{sec:ml}
 
   \emph{Generic preprocessors} provide a most general interface,
   transforming a list of function theorems to another
   list of function theorems, provided that neither the heading
-  constant nor its type change.  The @{const "0\<Colon>nat"} / @{const Suc}
+  constant nor its type change.  The @{term "0\<Colon>nat"} / @{const Suc}
   pattern elimination implemented in
   theory @{text "EfficientNat"} (\secref{eff_nat}) uses this
   interface.
@@ -646,7 +646,7 @@
 
 text {*
   Then code generation will fail.  Why?  The definition
-  of @{const "op \<le>"} depends on equality on both arguments,
+  of @{term "op \<le>"} depends on equality on both arguments,
   which are polymorphic and impose an additional @{text eq}
   class constraint, thus violating the type discipline
   for class operations.
@@ -740,7 +740,7 @@
 
 text {*
   \noindent prints a table with \emph{all} defining equations
-  for @{const "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}, including
+  for @{term "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}, including
   \emph{all} defining equations those equations depend
   on recursivly.  @{text "\<CODETHMS>"} provides a convenient
   mechanism to inspect the impact of a preprocessor setup
@@ -1027,7 +1027,7 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML Code.add_func: "bool -> thm -> theory -> theory"} \\
+  @{index_ML Code.add_func: "thm -> theory -> theory"} \\
   @{index_ML Code.del_func: "thm -> theory -> theory"} \\
   @{index_ML Code.add_funcl: "string * thm list Susp.T -> theory -> theory"} \\
   @{index_ML Code.add_inline: "thm -> theory -> theory"} \\