# HG changeset patch
# User wenzelm
# Date 1165510732 -3600
# Node ID 627c90b310c1714a7652ce8bc7b656468ac45159
# Parent  785c3d0242c53a0cf625c170793d6005be58a6bf
tuned print_locale output;
add_decls: Thm.internalK;

diff -r 785c3d0242c5 -r 627c90b310c1 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Dec 07 17:58:50 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Dec 07 17:58:52 2006 +0100
@@ -1469,7 +1469,8 @@
   let val (all_elems, ctxt) = read_expr import body (ProofContext.init thy) in
     Pretty.big_list "locale elements:" (all_elems
       |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
-      |> map (Pretty.chunks o Element.pretty_ctxt ctxt))
+      |> map (Element.pretty_ctxt ctxt) |> filter_out null
+      |> map Pretty.chunks)
     |> Pretty.writeln
   end;
 
@@ -1570,7 +1571,7 @@
   ProofContext.theory (change_locale loc
     (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
       (axiom, import, elems, params, lparams, add (decl, stamp ()) decls, regs, intros))) #>
-  add_thmss loc "" [(("", [Attrib.internal (decl_attrib decl)]), [([dummy_thm], [])])];
+  add_thmss loc Thm.internalK [(("", [Attrib.internal (decl_attrib decl)]), [([dummy_thm], [])])];
 
 in