--- a/src/Provers/classical.ML Fri Mar 16 14:46:13 2012 +0100
+++ b/src/Provers/classical.ML Fri Mar 16 18:20:12 2012 +0100
@@ -960,8 +960,7 @@
(** outer syntax **)
val _ =
- Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner"
- Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "print_claset"} "print context of Classical Reasoner"
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
Toplevel.keep (fn state =>
let val ctxt = Toplevel.context_of state