src/Pure/Isar/toplevel.ML

 (* print exceptions *)
 
 local
 
 fun with_context f xs =
-  (case Context.get_context () of NONE => []
+  (case ML_Context.get_context () of NONE => []
   | SOME context => map (f (Context.proof_of context)) xs);
 
 fun raised name [] = "exception " ^ name ^ " raised"
   | raised name [msg] = "exception " ^ name ^ " raised: " ^ msg
   | raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs);