Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned print_locale output;
authorwenzelm
Thu, 07 Dec 2006 17:58:52 +0100
changeset 21701 627c90b310c1
parent 21700 785c3d0242c5
child 21702 9300bec44e6a
tuned print_locale output; add_decls: Thm.internalK;
src/Pure/Isar/locale.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle