pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;
authorwenzelm
Fri Sep 12 10:54:00 2008 +0200 (2008-09-12 ago)
changeset 2820902f3222a392d
parent 28208 3a8b3453129a
child 28210 c164d1892553
pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Sep 11 22:22:59 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Sep 12 10:54:00 2008 +0200
     1.3 @@ -295,11 +295,13 @@
     1.4  fun pretty_thms ctxt [th] = pretty_thm ctxt th
     1.5    | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
     1.6  
     1.7 +val extern_fact = Facts.extern o facts_of;
     1.8 +
     1.9  fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths
    1.10    | pretty_fact ctxt (a, [th]) = Pretty.block
    1.11 -      [Pretty.str (NameSpace.base a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
    1.12 +      [Pretty.str (extern_fact ctxt a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
    1.13    | pretty_fact ctxt (a, ths) = Pretty.block
    1.14 -      (Pretty.fbreaks (Pretty.str (NameSpace.base a ^ ":") :: map (pretty_thm ctxt) ths));
    1.15 +      (Pretty.fbreaks (Pretty.str (extern_fact ctxt a ^ ":") :: map (pretty_thm ctxt) ths));
    1.16  
    1.17  val string_of_thm = Pretty.string_of oo pretty_thm;
    1.18