--- a/src/Tools/try.ML Fri Mar 16 14:46:13 2012 +0100
+++ b/src/Tools/try.ML Fri Mar 16 18:20:12 2012 +0100
@@ -88,9 +88,9 @@
|> tap (fn NONE => Output.urgent_message "Tried in vain." | _ => ())
val _ =
- Outer_Syntax.improper_command tryN
- "try a combination of automatic proving and disproving tools" Keyword.diag
- (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
+ 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)))
(* automatic try *)