equal
deleted
inserted
replaced
229 is_formula_too_complex ho_atp t orelse |
229 is_formula_too_complex ho_atp t orelse |
230 exists_type type_has_top_sort t orelse exists_technical_const t orelse |
230 exists_type type_has_top_sort t orelse exists_technical_const t orelse |
231 exists_low_level_class_const t orelse is_that_fact th |
231 exists_low_level_class_const t orelse is_that_fact th |
232 end |
232 end |
233 |
233 |
234 fun hackish_string_for_term ctxt t = |
234 fun hackish_string_for_term ctxt = |
235 Print_Mode.setmp |
235 with_vanilla_print_mode (Syntax.string_of_term ctxt) #> repair_printed_term |
236 (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) |
|
237 (Syntax.string_of_term ctxt) t |
|
238 |> String.translate (fn c => if Char.isPrint c then str c else "") |
|
239 |> simplify_spaces |
|
240 |
236 |
241 (* This is a terrible hack. Free variables are sometimes coded as "M__" when |
237 (* This is a terrible hack. Free variables are sometimes coded as "M__" when |
242 they are displayed as "M" and we want to avoid clashes with these. But |
238 they are displayed as "M" and we want to avoid clashes with these. But |
243 sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all |
239 sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all |
244 prefixes of all free variables. In the worse case scenario, where the fact |
240 prefixes of all free variables. In the worse case scenario, where the fact |