src/Tools/Code/code_ml.ML

   | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
 
 
 (** 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]) =
           concat [print_typ BR ty, (str o deresolve) tyco]
       | print_tyco_expr (tyco, tys) =

            of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
                 then print_case is_pseudo_fun some_thm vars fxy case_expr
                 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
             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
           else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]

 };
 
 
 (** 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]) =
           concat [print_typ BR ty, (str o deresolve) tyco]
       | print_tyco_expr (tyco, tys) =

            of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
                 then print_case is_pseudo_fun some_thm vars fxy case_expr
                 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
             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
           else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]

       ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
 
     (* 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 *)
     fun print_module _ base _ xs =
       let