src/Tools/Code/code_thingol.ML
changeset 47836 5c6955f487e5
parent 47542 919dfcdf6d8a
child 47876 421760a1efe7
     1.1 --- a/src/Tools/Code/code_thingol.ML	Fri Mar 16 14:46:13 2012 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Mar 16 18:20:12 2012 +0100
     1.3 @@ -1046,14 +1046,15 @@
     1.4  in
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.improper_command "code_thms" "print system of code equations for code" Keyword.diag
     1.8 +  Outer_Syntax.improper_command @{command_spec "code_thms"}
     1.9 +    "print system of code equations for code"
    1.10      (Scan.repeat1 Parse.term_group
    1.11        >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
    1.12          o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
    1.13  
    1.14  val _ =
    1.15 -  Outer_Syntax.improper_command "code_deps" "visualize dependencies of code equations for code"
    1.16 -    Keyword.diag
    1.17 +  Outer_Syntax.improper_command @{command_spec "code_deps"}
    1.18 +    "visualize dependencies of code equations for code"
    1.19      (Scan.repeat1 Parse.term_group
    1.20        >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
    1.21          o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));