equal
deleted
inserted
replaced
65 Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false) |
65 Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false) |
66 |
66 |
67 val no_fact_override = {add = [], del = [], only = false} |
67 val no_fact_override = {add = [], del = [], only = false} |
68 |
68 |
69 fun needs_quoting keywords s = |
69 fun needs_quoting keywords s = |
70 Keyword.is_keyword keywords s orelse |
70 Keyword.is_literal keywords s orelse |
71 exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s) |
71 exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s) |
72 |
72 |
73 fun make_name keywords multi j name = |
73 fun make_name keywords multi j name = |
74 (name |> needs_quoting keywords name ? quote) ^ |
74 (name |> needs_quoting keywords name ? quote) ^ |
75 (if multi then "(" ^ string_of_int j ^ ")" else "") |
75 (if multi then "(" ^ string_of_int j ^ ")" else "") |