equal
deleted
inserted
replaced
36 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = |
36 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = |
37 struct |
37 struct |
38 |
38 |
39 fun plural_s n = if n = 1 then "" else "s" |
39 fun plural_s n = if n = 1 then "" else "s" |
40 |
40 |
41 val serial_commas = ATP_Proof.serial_commas |
41 val serial_commas = Try.serial_commas |
42 val simplify_spaces = ATP_Proof.strip_spaces false (K true) |
42 val simplify_spaces = ATP_Proof.strip_spaces false (K true) |
43 |
43 |
44 fun parse_bool_option option name s = |
44 fun parse_bool_option option name s = |
45 (case s of |
45 (case s of |
46 "smart" => if option then NONE else raise Option |
46 "smart" => if option then NONE else raise Option |
229 case subst_for t of |
229 case subst_for t of |
230 SOME subst => monomorphic_term subst t |
230 SOME subst => monomorphic_term subst t |
231 | NONE => raise Type.TYPE_MATCH |
231 | NONE => raise Type.TYPE_MATCH |
232 end |
232 end |
233 |
233 |
234 val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal |
234 val subgoal_count = Try.subgoal_count |
235 |
235 |
236 fun strip_subgoal ctxt goal i = |
236 fun strip_subgoal ctxt goal i = |
237 let |
237 let |
238 val (t, (frees, params)) = |
238 val (t, (frees, params)) = |
239 Logic.goal_params (prop_of goal) i |
239 Logic.goal_params (prop_of goal) i |