--- 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 ->