changeset 30280 | eb98b49ef835 |
parent 29606 | fedb8be05f24 |
child 30364 | 577edc39b501 |
--- a/src/Pure/Isar/proof_display.ML Thu Mar 05 11:58:53 2009 +0100 +++ b/src/Pure/Isar/proof_display.ML Thu Mar 05 12:08:00 2009 +0100 @@ -75,7 +75,7 @@ fun pretty_fact_name (kind, "") = Pretty.str kind | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1, - Pretty.str (NameSpace.base name), Pretty.str ":"]; + Pretty.str (NameSpace.base_name name), Pretty.str ":"]; fun pretty_facts ctxt = flat o (separate [Pretty.fbrk, Pretty.str "and "]) o