equal
deleted
inserted
replaced
170 |
170 |
171 fun is_bad_query ctxt step j th isar_deps = |
171 fun is_bad_query ctxt step j th isar_deps = |
172 j mod step <> 0 orelse |
172 j mod step <> 0 orelse |
173 Thm.legacy_get_kind th = "" orelse |
173 Thm.legacy_get_kind th = "" orelse |
174 null (the_list isar_deps) orelse |
174 null (the_list isar_deps) orelse |
175 is_blacklisted_or_something (Thm.get_name_hint th) |
175 is_blacklisted_or_something (Thm_Name.short (Thm.get_name_hint th)) |
176 |
176 |
177 fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name = |
177 fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name = |
178 let |
178 let |
179 val path = Path.explode file_name |
179 val path = Path.explode file_name |
180 val facts = all_facts ctxt |
180 val facts = all_facts ctxt |