equal
deleted
inserted
replaced
278 val indent_size = 2 |
278 val indent_size = 2 |
279 |
279 |
280 val maybe_quote = ATP_Util.maybe_quote |
280 val maybe_quote = ATP_Util.maybe_quote |
281 |
281 |
282 fun pretty_maybe_quote keywords pretty = |
282 fun pretty_maybe_quote keywords pretty = |
283 let val s = Pretty.str_of pretty in |
283 let val s = Pretty.unformatted_string_of pretty |
284 if maybe_quote keywords s = s then pretty else Pretty.quote pretty |
284 in if maybe_quote keywords s = s then pretty else Pretty.quote pretty end |
285 end |
|
286 |
285 |
287 val hashw = ATP_Util.hashw |
286 val hashw = ATP_Util.hashw |
288 val hashw_string = ATP_Util.hashw_string |
287 val hashw_string = ATP_Util.hashw_string |
289 |
288 |
290 fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2) |
289 fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2) |