pretty_thm_aux: observe asms context;
authorwenzelm
Sat Sep 17 12:18:03 2005 +0200 (2005-09-17)
changeset 174473a23acfdf5ba
parent 17446 f869b73b71ec
child 17448 b94e2897776a
pretty_thm_aux: observe asms context;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Sat Sep 17 12:18:02 2005 +0200
     1.2 +++ b/src/Pure/display.ML	Sat Sep 17 12:18:03 2005 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  sig
     1.5    include BASIC_DISPLAY
     1.6    val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
     1.7 -  val pretty_thm_aux: Pretty.pp -> bool -> thm -> Pretty.T
     1.8 +  val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
     1.9    val pretty_thm_no_quote: thm -> Pretty.T
    1.10    val pretty_thm: thm -> Pretty.T
    1.11    val pretty_thms: thm list -> Pretty.T
    1.12 @@ -66,8 +66,9 @@
    1.13  fun pretty_flexpair pp (t, u) = Pretty.block
    1.14    [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
    1.15  
    1.16 -fun pretty_thm_aux pp quote th =
    1.17 +fun pretty_thm_aux pp quote show_hyps' asms raw_th =
    1.18    let
    1.19 +    val th = Thm.strip_shyps raw_th;
    1.20      val {hyps, tpairs, prop, der = (ora, _), ...} = Thm.rep_thm th;
    1.21      val xshyps = Thm.extra_shyps th;
    1.22      val (_, tags) = Thm.get_name_tags th;
    1.23 @@ -75,12 +76,13 @@
    1.24      val q = if quote then Pretty.quote else I;
    1.25      val prt_term = q o (Pretty.term pp);
    1.26  
    1.27 -    val hlen = length xshyps + length hyps + length tpairs;
    1.28 +    val hyps' = if ! show_hyps then hyps else fold (remove (op =)) asms hyps;
    1.29 +    val hlen = length xshyps + length hyps' + length tpairs;
    1.30      val hsymbs =
    1.31        if hlen = 0 andalso not ora then []
    1.32 -      else if ! show_hyps then
    1.33 +      else if ! show_hyps orelse show_hyps' then
    1.34          [Pretty.brk 2, Pretty.list "[" "]"
    1.35 -          (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps @
    1.36 +          (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @
    1.37             map (Pretty.sort pp) xshyps @
    1.38              (if ora then [Pretty.str "!"] else []))]
    1.39        else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^
    1.40 @@ -91,7 +93,7 @@
    1.41    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    1.42  
    1.43  fun gen_pretty_thm quote th =
    1.44 -  pretty_thm_aux (Sign.pp (Thm.theory_of_thm th)) quote th;
    1.45 +  pretty_thm_aux (Sign.pp (Thm.theory_of_thm th)) quote false [] th;
    1.46  
    1.47  val pretty_thm = gen_pretty_thm true;
    1.48  val pretty_thm_no_quote = gen_pretty_thm false;