equal
deleted
inserted
replaced
74 val (_, tags) = Thm.get_name_tags th; |
74 val (_, tags) = Thm.get_name_tags th; |
75 |
75 |
76 val q = if quote then Pretty.quote else I; |
76 val q = if quote then Pretty.quote else I; |
77 val prt_term = q o (Pretty.term pp); |
77 val prt_term = q o (Pretty.term pp); |
78 |
78 |
79 val hyps' = if ! show_hyps then hyps else fold (remove (op =)) asms hyps; |
79 val hyps' = if ! show_hyps then hyps else fold (remove (op aconv)) asms hyps; |
80 val hlen = length xshyps + length hyps' + length tpairs; |
80 val hlen = length xshyps + length hyps' + length tpairs; |
81 val hsymbs = |
81 val hsymbs = |
82 if hlen = 0 andalso not ora then [] |
82 if hlen = 0 andalso not ora then [] |
83 else if ! show_hyps orelse show_hyps' then |
83 else if ! show_hyps orelse show_hyps' then |
84 [Pretty.brk 2, Pretty.list "[" "]" |
84 [Pretty.brk 2, Pretty.list "[" "]" |