diff -r 61276a7fc369 -r dd04a8b654fc src/Doc/IsarImplementation/Proof.thy
--- a/src/Doc/IsarImplementation/Proof.thy	Tue Dec 31 11:19:14 2013 +0100
+++ b/src/Doc/IsarImplementation/Proof.thy	Tue Dec 31 14:29:16 2013 +0100
@@ -279,7 +279,7 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML_type Assumption.export} \\
-  @{index_ML Assumption.assume: "cterm -> thm"} \\
+  @{index_ML Assumption.assume: "Proof.context -> cterm -> thm"} \\
   @{index_ML Assumption.add_assms:
     "Assumption.export ->
   cterm list -> Proof.context -> thm list * Proof.context"} \\
@@ -296,7 +296,7 @@
   and the @{ML_type "cterm list"} the collection of assumptions to be
   discharged simultaneously.
 
-  \item @{ML Assumption.assume}~@{text "A"} turns proposition @{text
+  \item @{ML Assumption.assume}~@{text "ctxt A"} turns proposition @{text
   "A"} into a primitive assumption @{text "A \<turnstile> A'"}, where the
   conclusion @{text "A'"} is in HHF normal form.