src/Doc/IsarImplementation/Proof.thy

 *}
 
 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"} \\
   @{index_ML Assumption.add_assumes: "
   cterm list -> Proof.context -> thm list * Proof.context"} \\

   rules, which is any function of type @{ML_type "bool -> cterm list
   -> thm -> thm"}, where the @{ML_type "bool"} indicates goal mode,
   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.
 
   \item @{ML Assumption.add_assms}~@{text "r As"} augments the context
   by assumptions @{text "As"} with export rule @{text "r"}.  The