src/Pure/Isar/proof_display.ML
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