diff -r c25aa1c50ce9 -r 3cbce59ed78d doc-src/IsarImplementation/Thy/Logic.thy
--- 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