--- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Apr 26 07:47:18 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Mon Apr 26 11:20:18 2010 +0200
@@ -128,8 +128,7 @@
@{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
@{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
@{index_ML Sign.add_types: "(binding * int * mixfix) list -> theory -> theory"} \\
- @{index_ML Sign.add_tyabbrs_i: "
- (binding * string list * typ * mixfix) list -> theory -> theory"} \\
+ @{index_ML Sign.add_type_abbrev: "binding * string list * typ -> theory -> theory"} \\
@{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\
@{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
@{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
@@ -168,9 +167,9 @@
type constructors @{text "\<kappa>"} with @{text "k"} arguments and
optional mixfix syntax.
- \item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
- defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"} with
- optional mixfix syntax.
+ \item @{ML Sign.add_type_abbrev}~@{text "(\<kappa>, \<^vec>\<alpha>,
+ \<tau>)"} defines a new type abbreviation @{text
+ "(\<^vec>\<alpha>)\<kappa> = \<tau>"}.
\item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
c\<^isub>n])"} declares a new class @{text "c"}, together with class