more procise printing of fact names;
authorwenzelm
Fri Sep 12 12:04:16 2008 +0200 (2008-09-12)
changeset 28210c164d1892553
parent 28209 02f3222a392d
child 28211 07cfaa1a9e12
more procise printing of fact names;
src/Pure/Isar/calculation.ML
src/Pure/Isar/proof_display.ML
     1.1 --- a/src/Pure/Isar/calculation.ML	Fri Sep 12 10:54:00 2008 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Fri Sep 12 12:04:16 2008 +0200
     1.3 @@ -114,8 +114,8 @@
     1.4    | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc;
     1.5  
     1.6  fun print_calculation false _ _ = ()
     1.7 -  | print_calculation true ctxt calc =
     1.8 -      Pretty.writeln (ProofContext.pretty_fact ctxt (calculationN, calc));
     1.9 +  | print_calculation true ctxt calc = Pretty.writeln
    1.10 +      (ProofContext.pretty_fact ctxt (ProofContext.full_name ctxt calculationN, calc));
    1.11  
    1.12  
    1.13  (* also and finally *)
     2.1 --- a/src/Pure/Isar/proof_display.ML	Fri Sep 12 10:54:00 2008 +0200
     2.2 +++ b/src/Pure/Isar/proof_display.ML	Fri Sep 12 12:04:16 2008 +0200
     2.3 @@ -46,8 +46,8 @@
     2.4  fun pretty_theorems_diff prev_thys thy =
     2.5    let
     2.6      val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy);
     2.7 -    val thmss = Facts.extern_static (map PureThy.facts_of prev_thys) (PureThy.facts_of thy);
     2.8 -  in Pretty.big_list "theorems:" (map pretty_fact thmss) end;
     2.9 +    val thmss = Facts.dest_static (map PureThy.facts_of prev_thys) (PureThy.facts_of thy);
    2.10 +  in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
    2.11  
    2.12  fun print_theorems_diff prev_thy thy =
    2.13    Pretty.writeln (pretty_theorems_diff [prev_thy] thy);