src/Pure/Isar/isar_cmd.ML

   val print_context: Toplevel.transition -> Toplevel.transition
   val print_theory: Toplevel.transition -> Toplevel.transition
   val print_syntax: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
-  val print_locale: Locale.expr * Locale.element list
+  val print_locale: bool * (Locale.expr * Locale.element list)
     -> Toplevel.transition -> Toplevel.transition
   val print_registrations: bool -> string -> Toplevel.transition -> Toplevel.transition
   val print_attributes: Toplevel.transition -> Toplevel.transition
   val print_simpset: Toplevel.transition -> Toplevel.transition
   val print_rules: Toplevel.transition -> Toplevel.transition

   | _ => PureThy.print_theorems) (Toplevel.theory_of state)) o print_theorems_proof;
 
 val print_locales = Toplevel.unknown_theory o
   Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
 
-fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  Locale.print_locale (Toplevel.theory_of state) import body);
+fun print_locale (show_facts, (import, body)) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
+  Locale.print_locale (Toplevel.theory_of state) show_facts import body);
 
 fun print_registrations show_wits name = Toplevel.unknown_context o
   Toplevel.keep (Toplevel.node_case (Locale.print_global_registrations show_wits name)
     (Locale.print_local_registrations show_wits name o Proof.context_of));