src/Tools/subtyping.ML
changeset 46961 5c6955f487e5
parent 46665 919dfcdf6d8a
child 47060 e2741ec9ae36
--- a/src/Tools/subtyping.ML	Fri Mar 16 14:46:13 2012 +0100
+++ b/src/Tools/subtyping.ML	Fri Mar 16 18:20:12 2012 +0100
@@ -1028,10 +1028,10 @@
 (* outer syntax commands *)
 
 val _ =
-  Outer_Syntax.improper_command "print_coercions" "print all coercions" Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "print_coercions"} "print all coercions"
     (Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)))
 val _ =
-  Outer_Syntax.improper_command "print_coercion_maps" "print all coercion maps" Keyword.diag
+  Outer_Syntax.improper_command @{command_spec "print_coercion_maps"} "print all coercion maps"
     (Scan.succeed (Toplevel.keep (print_coercion_maps o Toplevel.context_of)))
 
 end;