equal
deleted
inserted
replaced
357 else |
357 else |
358 error ("Unknown subcommand: " ^ quote subcommand ^ ".") |
358 error ("Unknown subcommand: " ^ quote subcommand ^ ".") |
359 end |
359 end |
360 |
360 |
361 fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) = |
361 fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) = |
362 Toplevel.unknown_proof o |
|
363 Toplevel.keep (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of) |
362 Toplevel.keep (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of) |
364 |
363 |
365 fun string_of_raw_param (key, values) = |
364 fun string_of_raw_param (key, values) = |
366 key ^ (case implode_param values of "" => "" | value => " = " ^ value) |
365 key ^ (case implode_param values of "" => "" | value => " = " ^ value) |
367 |
366 |