equal
deleted
inserted
replaced
113 raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`" |
113 raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`" |
114 fun fact_from_ref ctxt reserved chained_ths (xthm as (xref, args)) = |
114 fun fact_from_ref ctxt reserved chained_ths (xthm as (xref, args)) = |
115 let |
115 let |
116 val ths = Attrib.eval_thms ctxt [xthm] |
116 val ths = Attrib.eval_thms ctxt [xthm] |
117 val bracket = |
117 val bracket = |
118 implode (map (fn arg => "[" ^ Pretty.str_of (Args.pretty_src ctxt arg) |
118 map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args |
119 ^ "]") args) |
119 |> implode |
120 fun nth_name j = |
120 fun nth_name j = |
121 case xref of |
121 case xref of |
122 Facts.Fact s => backquote s ^ bracket |
122 Facts.Fact s => backquote s ^ bracket |
123 | Facts.Named (("", _), _) => "[" ^ bracket ^ "]" |
123 | Facts.Named (("", _), _) => "[" ^ bracket ^ "]" |
124 | Facts.Named ((name, _), NONE) => |
124 | Facts.Named ((name, _), NONE) => |