--- a/src/Tools/Code/code_thingol.ML Fri Mar 16 14:46:13 2012 +0100
+++ b/src/Tools/Code/code_thingol.ML Fri Mar 16 18:20:12 2012 +0100
@@ -1046,14 +1046,15 @@
in
val _ =
- Outer_Syntax.improper_command "code_thms" "print system of code equations for code" Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "code_thms"}
+ "print system of code equations for code"
(Scan.repeat1 Parse.term_group
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
val _ =
- Outer_Syntax.improper_command "code_deps" "visualize dependencies of code equations for code"
- Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "code_deps"}
+ "visualize dependencies of code equations for code"
(Scan.repeat1 Parse.term_group
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));