# HG changeset patch
# User wenzelm
# Date 1221213856 -7200
# Node ID c164d1892553937e407961dc8c93d3763a32110c
# Parent  02f3222a392d23362b0efa83bff7f16c2d2f909b
more procise printing of fact names;

diff -r 02f3222a392d -r c164d1892553 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Fri Sep 12 10:54:00 2008 +0200
+++ b/src/Pure/Isar/calculation.ML	Fri Sep 12 12:04:16 2008 +0200
@@ -114,8 +114,8 @@
   | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc;
 
 fun print_calculation false _ _ = ()
-  | print_calculation true ctxt calc =
-      Pretty.writeln (ProofContext.pretty_fact ctxt (calculationN, calc));
+  | print_calculation true ctxt calc = Pretty.writeln
+      (ProofContext.pretty_fact ctxt (ProofContext.full_name ctxt calculationN, calc));
 
 
 (* also and finally *)
diff -r 02f3222a392d -r c164d1892553 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Fri Sep 12 10:54:00 2008 +0200
+++ b/src/Pure/Isar/proof_display.ML	Fri Sep 12 12:04:16 2008 +0200
@@ -46,8 +46,8 @@
 fun pretty_theorems_diff prev_thys thy =
   let
     val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy);
-    val thmss = Facts.extern_static (map PureThy.facts_of prev_thys) (PureThy.facts_of thy);
-  in Pretty.big_list "theorems:" (map pretty_fact thmss) end;
+    val thmss = Facts.dest_static (map PureThy.facts_of prev_thys) (PureThy.facts_of thy);
+  in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
 
 fun print_theorems_diff prev_thy thy =
   Pretty.writeln (pretty_theorems_diff [prev_thy] thy);