equal
deleted
inserted
replaced
86 val src = Src; |
86 val src = Src; |
87 fun dest_src (Src src) = src; |
87 fun dest_src (Src src) = src; |
88 |
88 |
89 fun pretty_src ctxt src = |
89 fun pretty_src ctxt src = |
90 let |
90 let |
91 val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt; |
91 val prt_thm = Pretty.backquote o Display.pretty_thm ctxt; |
92 fun prt arg = |
92 fun prt arg = |
93 (case T.get_value arg of |
93 (case T.get_value arg of |
94 SOME (T.Text s) => Pretty.str (quote s) |
94 SOME (T.Text s) => Pretty.str (quote s) |
95 | SOME (T.Typ T) => Syntax.pretty_typ ctxt T |
95 | SOME (T.Typ T) => Syntax.pretty_typ ctxt T |
96 | SOME (T.Term t) => Syntax.pretty_term ctxt t |
96 | SOME (T.Term t) => Syntax.pretty_term ctxt t |