59 [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u]; |
59 [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u]; |
60 |
60 |
61 fun pretty_thm_aux pp quote show_hyps' asms raw_th = |
61 fun pretty_thm_aux pp quote show_hyps' asms raw_th = |
62 let |
62 let |
63 val th = Thm.strip_shyps raw_th; |
63 val th = Thm.strip_shyps raw_th; |
64 val {hyps, tpairs, prop, der = (ora, _), ...} = Thm.rep_thm th; |
64 val {hyps, tpairs, prop, der, ...} = Thm.rep_thm th; |
65 val xshyps = Thm.extra_shyps th; |
65 val xshyps = Thm.extra_shyps th; |
66 val tags = Thm.get_tags th; |
66 val tags = Thm.get_tags th; |
67 |
67 |
68 val q = if quote then Pretty.quote else I; |
68 val q = if quote then Pretty.quote else I; |
69 val prt_term = q o Pretty.term pp; |
69 val prt_term = q o Pretty.term pp; |
70 |
70 |
71 val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps; |
71 val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps; |
72 val ora' = ora andalso (! show_hyps orelse not (! quick_and_dirty)); |
72 val ora' = Deriv.oracle_of der andalso (! show_hyps orelse not (! quick_and_dirty)); |
73 val hlen = length xshyps + length hyps' + length tpairs; |
73 val hlen = length xshyps + length hyps' + length tpairs; |
74 val hsymbs = |
74 val hsymbs = |
75 if hlen = 0 andalso not ora' then [] |
75 if hlen = 0 andalso not ora' then [] |
76 else if ! show_hyps orelse show_hyps' then |
76 else if ! show_hyps orelse show_hyps' then |
77 [Pretty.brk 2, Pretty.list "[" "]" |
77 [Pretty.brk 2, Pretty.list "[" "]" |