# HG changeset patch
# User haftmann
# Date 1356638468 -3600
# Node ID e3d25e751d05c93a937f2ff668ef7f0aceda9db7
# Parent  4d0997abce796f08857ffa0d6c11cded3e33d88f
more explicit name

diff -r 4d0997abce79 -r e3d25e751d05 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Dec 27 16:49:12 2012 +0100
+++ b/src/Tools/Code/code_ml.ML	Thu Dec 27 21:01:08 2012 +0100
@@ -51,7 +51,7 @@
 
 (** SML serializer **)
 
-fun print_sml_stmt tyco_syntax const_syntax reserved is_cons deresolve =
+fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   let
     fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
       | print_tyco_expr (tyco, [ty]) =
@@ -110,7 +110,7 @@
                 else print_app is_pseudo_fun some_thm vars fxy app
             | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
     and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
-      if is_cons c then
+      if is_constr c then
         let val k = length dom in
           if k < 2 orelse length ts = k
           then (str o deresolve) c
@@ -355,7 +355,7 @@
 
 (** OCaml serializer **)
 
-fun print_ocaml_stmt tyco_syntax const_syntax reserved is_cons deresolve =
+fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   let
     fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
       | print_tyco_expr (tyco, [ty]) =
@@ -410,7 +410,7 @@
                 else print_app is_pseudo_fun some_thm vars fxy app
             | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
     and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
-      if is_cons c then
+      if is_constr c then
         let val k = length dom in
           if length ts = k
           then (str o deresolve) c
@@ -794,7 +794,7 @@
     (* print statements *)
     fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
       tyco_syntax const_syntax (make_vars reserved_syms)
-      (Code_Thingol.is_cons program) (deresolver prefix_fragments) stmt
+      (Code_Thingol.is_constr program) (deresolver prefix_fragments) stmt
       |> apfst SOME;
 
     (* print modules *)
diff -r 4d0997abce79 -r e3d25e751d05 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Dec 27 16:49:12 2012 +0100
+++ b/src/Tools/Code/code_thingol.ML	Thu Dec 27 21:01:08 2012 +0100
@@ -84,7 +84,7 @@
   val empty_funs: program -> string list
   val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
   val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
-  val is_cons: program -> string -> bool
+  val is_constr: program -> string -> bool
   val is_case: stmt -> bool
   val labelled_name: theory -> program -> string -> string
   val group_stmts: theory -> program
@@ -464,7 +464,7 @@
           inst_params = map_classparam_instances_as_term f inst_params,
           superinst_params = map_classparam_instances_as_term f superinst_params };
 
-fun is_cons program name = case Graph.get_node program name
+fun is_constr program name = case Graph.get_node program name
  of Datatypecons _ => true
   | _ => false;