src/Pure/Isar/isar_cmd.ML

   val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
   val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
   val print_context: Toplevel.transition -> Toplevel.transition
   val print_theory: bool -> Toplevel.transition -> Toplevel.transition
   val print_syntax: Toplevel.transition -> Toplevel.transition
+  val print_abbrevs: Toplevel.transition -> Toplevel.transition
   val print_facts: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
   val print_locale: bool * (Locale.expr * Element.context list)
     -> Toplevel.transition -> Toplevel.transition

 val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART);
 
 val welcome = Toplevel.imperative (writeln o Session.welcome);
 
 val exit = Toplevel.keep (fn state =>
-  (Context.set_context (try Toplevel.theory_of state);
-    writeln "Leaving the Isar loop.  Invoke 'Isar.loop();' to continue.";
-    raise Toplevel.TERMINATE));
+  (Context.set_context (try Toplevel.theory_of state); raise Toplevel.TERMINATE));
 
 val quit = Toplevel.imperative quit;
 
 
 (* touch theories *)

 fun print_theory verbose = Toplevel.unknown_theory o
   Toplevel.keep (ProofDisplay.print_full_theory verbose o Toplevel.theory_of);
 
 val print_syntax = Toplevel.unknown_context o
   Toplevel.keep (ProofContext.print_syntax o Toplevel.context_of);
+
+val print_abbrevs = Toplevel.unknown_context o
+  Toplevel.keep (ProofContext.print_abbrevs o Toplevel.context_of);
 
 val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state =>
   ProofContext.setmp_verbose
     ProofContext.print_lthms (Toplevel.context_of state));