# HG changeset patch
# User haftmann
# Date 1235150951 -3600
# Node ID 5e9d471afef390d15d447f90653375256791008d
# Parent  55954f7260431a8c68ecebaf941d54fdfda37b59
consequent use of term `code equation`

diff -r 55954f726043 -r 5e9d471afef3 src/Tools/code/code_funcgr.ML
--- a/src/Tools/code/code_funcgr.ML	Fri Feb 20 18:29:10 2009 +0100
+++ b/src/Tools/code/code_funcgr.ML	Fri Feb 20 18:29:11 2009 +0100
@@ -317,13 +317,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)));
diff -r 55954f726043 -r 5e9d471afef3 src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Fri Feb 20 18:29:10 2009 +0100
+++ b/src/Tools/code/code_target.ML	Fri Feb 20 18:29:11 2009 +0100
@@ -418,7 +418,7 @@
     val program4 = Graph.subgraph (member (op =) names_all) program3;
     val empty_funs = filter_out (member (op =) abortable)
       (Code_Thingol.empty_funs program3);
-    val _ = if null empty_funs then () else error ("No defining equations for "
+    val _ = if null empty_funs then () else error ("No code equations for "
       ^ commas (map (Sign.extern_const thy) empty_funs));
   in
     serializer module args (labelled_name thy program2) reserved includes
diff -r 55954f726043 -r 5e9d471afef3 src/Tools/code/code_wellsorted.ML
--- 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)));