changeset 51557 | 4e4b56b7a3a5 |
parent 46961 | 5c6955f487e5 |
child 51594 | 89bfe7a33615 |
--- a/src/Tools/try.ML Wed Mar 27 17:55:21 2013 +0100 +++ b/src/Tools/try.ML Wed Mar 27 17:58:07 2013 +0100 @@ -90,7 +90,7 @@ val _ = Outer_Syntax.improper_command @{command_spec "try"} "try a combination of automatic proving and disproving tools" - (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of))) + (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of))) (* automatic try *)