diff -r f6e8293747fd -r 48dd1cefb4ae src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy	Sun Jul 05 15:02:30 2015 +0200
@@ -656,7 +656,8 @@
   @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
   @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
   @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
-  @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
+  @{index_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
+  -> thm -> thm"} \\
   @{index_ML Thm.add_axiom: "Proof.context ->
   binding * term -> theory -> (string * thm) * theory"} \\
   @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->