diff -r 05d4e5f660ae -r 10b89c127153 doc-src/IsarImplementation/Thy/Prelim.thy --- a/doc-src/IsarImplementation/Thy/Prelim.thy Sun Aug 26 22:23:10 2012 +0200 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Sun Aug 26 22:32:22 2012 +0200 @@ -157,7 +157,7 @@ @{index_ML Theory.checkpoint: "theory -> theory"} \\ @{index_ML Theory.copy: "theory -> theory"} \\ @{index_ML Theory.merge: "theory * theory -> theory"} \\ - @{index_ML Theory.begin_theory: "string -> theory list -> theory"} \\ + @{index_ML Theory.begin_theory: "string * Position.T -> theory list -> theory"} \\ @{index_ML Theory.parents_of: "theory -> theory list"} \\ @{index_ML Theory.ancestors_of: "theory -> theory list"} \\ \end{mldecls}