src/Pure/Thy/thm_database.ML

 fun warn_ml name =
   if is_ml_identifier name then false
   else if name = "" then true
   else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
 
-val use_text_verbose = use_text Context.ml_output true;
+val use_text_verbose = use_text Output.ml_output true;
 
 fun ml_store_thm (name, thm) =
   let val thm' = store_thm (name, thm) in
     if warn_ml name then ()
     else (qed_thms := [thm'];