src/Pure/Isar/proof_display.ML
changeset 50126 3dec88149176
parent 49867 d3053a55bfcb
child 51584 98029ceda8ce
     1.1 --- a/src/Pure/Isar/proof_display.ML	Mon Nov 19 18:01:48 2012 +0100
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Mon Nov 19 20:23:47 2012 +0100
     1.3 @@ -46,10 +46,8 @@
     1.4    | NONE => Syntax.init_pretty_global thy0);
     1.5  
     1.6  fun pp_thm th =
     1.7 -  let
     1.8 -    val ctxt = default_context (Thm.theory_of_thm th);
     1.9 -    val flags = {quote = true, show_hyps = false, show_status = true};
    1.10 -  in Display.pretty_thm_raw ctxt flags th end;
    1.11 +  let val ctxt = default_context (Thm.theory_of_thm th);
    1.12 +  in Display.pretty_thm_raw ctxt {quote = true, show_hyps = false} th end;
    1.13  
    1.14  fun pp_typ thy T = Pretty.quote (Syntax.pretty_typ (default_context thy) T);
    1.15  fun pp_term thy t = Pretty.quote (Syntax.pretty_term (default_context thy) t);
    1.16 @@ -85,7 +83,7 @@
    1.17  
    1.18  fun pretty_rule ctxt s thm =
    1.19    Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
    1.20 -    Pretty.fbrk, Display.pretty_thm_aux ctxt false thm];
    1.21 +    Pretty.fbrk, Display.pretty_thm ctxt thm];
    1.22  
    1.23  val string_of_rule = Pretty.string_of ooo pretty_rule;
    1.24  
    1.25 @@ -138,7 +136,7 @@
    1.26  
    1.27  fun pretty_facts ctxt =
    1.28    flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o
    1.29 -    map (single o Proof_Context.pretty_fact_aux ctxt false);
    1.30 +    map (single o Proof_Context.pretty_fact ctxt);
    1.31  
    1.32  in
    1.33  
    1.34 @@ -151,7 +149,7 @@
    1.35      (Pretty.writeln o Pretty.mark markup)
    1.36        (case facts of
    1.37          [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
    1.38 -          Proof_Context.pretty_fact_aux ctxt false fact])
    1.39 +          Proof_Context.pretty_fact ctxt fact])
    1.40        | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
    1.41            Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
    1.42