src/Tools/code/code_wellsorted.ML
changeset 30024 5e9d471afef3
parent 30010 862fc7751a15
child 30029 d14d0b4bf5b4
--- a/src/Tools/code/code_wellsorted.ML	Fri Feb 20 18:29:10 2009 +0100
+++ b/src/Tools/code/code_wellsorted.ML	Fri Feb 20 18:29:11 2009 +0100
@@ -388,13 +388,13 @@
 in
 
 val _ =
-  OuterSyntax.improper_command "code_thms" "print system of defining equations for code" OuterKeyword.diag
+  OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
     (Scan.repeat P.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 _ =
-  OuterSyntax.improper_command "code_deps" "visualize dependencies of defining equations for code" OuterKeyword.diag
+  OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
     (Scan.repeat P.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)));