src/Provers/classical.ML
changeset 46961 5c6955f487e5
parent 46874 993c413746f4
child 48126 cdbdbfa6a29f
     1.1 --- a/src/Provers/classical.ML	Fri Mar 16 14:46:13 2012 +0100
     1.2 +++ b/src/Provers/classical.ML	Fri Mar 16 18:20:12 2012 +0100
     1.3 @@ -960,8 +960,7 @@
     1.4  (** outer syntax **)
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner"
     1.8 -    Keyword.diag
     1.9 +  Outer_Syntax.improper_command @{command_spec "print_claset"} "print context of Classical Reasoner"
    1.10      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    1.11        Toplevel.keep (fn state =>
    1.12          let val ctxt = Toplevel.context_of state