96 find_suggested_facts (map (rpair 1.0) isar_deps) facts |
96 find_suggested_facts (map (rpair 1.0) isar_deps) facts |
97 (* adapted from "mirabelle_sledgehammer.ML" *) |
97 (* adapted from "mirabelle_sledgehammer.ML" *) |
98 fun set_file_name heading (SOME dir) = |
98 fun set_file_name heading (SOME dir) = |
99 let |
99 let |
100 val prob_prefix = |
100 val prob_prefix = |
101 "goal_" ^ string_of_int j ^ "__" ^ escape_meta name ^ "__" ^ |
101 "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^ |
102 heading |
102 heading |
103 in |
103 in |
104 Config.put dest_dir dir |
104 Config.put dest_dir dir |
105 #> Config.put problem_prefix (prob_prefix ^ "__") |
105 #> Config.put problem_prefix (prob_prefix ^ "__") |
106 #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix) |
106 #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix) |
107 end |
107 end |
108 | set_file_name _ NONE = I |
108 | set_file_name _ NONE = I |
109 fun prove heading get facts = |
109 fun prove heading get facts = |
110 let |
110 let |
111 fun nickify ((_, stature), th) = |
111 fun nickify ((_, stature), th) = |
112 ((K (escape_meta (nickname_of_thm th)), stature), th) |
112 ((K (encode_str (nickname_of_thm th)), stature), th) |
113 val facts = |
113 val facts = |
114 facts |
114 facts |
115 |> map (get #> nickify) |
115 |> map (get #> nickify) |
116 |> maybe_instantiate_inducts ctxt hyp_ts concl_t |
116 |> maybe_instantiate_inducts ctxt hyp_ts concl_t |
117 |> take (the max_facts) |
117 |> take (the max_facts) |