changeset 60094 | 96a4765ba7d1 |
parent 59962 | b622365f181c |
child 60190 | 906de96ba68a |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Apr 16 13:48:10 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Apr 16 14:18:32 2015 +0200 @@ -359,7 +359,6 @@ end fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) = - Toplevel.unknown_proof o Toplevel.keep (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of) fun string_of_raw_param (key, values) =