src/Tools/Code/code_ml.ML

   | ML_Val of ml_binding
   | ML_Funs of ml_binding list * string list
   | ML_Datas of (string * ((vname * sort) list * ((string * vname list) * itype list) list)) list
   | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
 
-fun stmt_name_of_binding (ML_Function (name, _)) = name
-  | stmt_name_of_binding (ML_Instance (name, _)) = name;
-
 fun print_product _ [] = NONE
   | print_product print [x] = SOME (print x)
   | print_product print xs = (SOME o enum " *" "" "") (map print xs);
 
 fun tuplify _ _ [] = NONE

 
 (** SML serializer **)
 
 fun print_sml_stmt tyco_syntax const_syntax reserved is_cons deresolve =
   let
-    fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
-      | print_tyco_expr fxy (tyco, [ty]) =
+    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 fxy (tyco, tys) =
+      | print_tyco_expr (tyco, tys) =
           concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
     and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
-         of NONE => print_tyco_expr fxy (tyco, tys)
-          | SOME (i, print) => print print_typ fxy tys)
+         of NONE => print_tyco_expr (tyco, tys)
+          | SOME (_, print) => print print_typ fxy tys)
       | print_typ fxy (ITyVar v) = str ("'" ^ v);
-    fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
+    fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]);
     fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
       (map_filter (fn (v, sort) =>
         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);

       (print_term is_pseudo_fun) const_syntax some_thm vars
     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
     and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
-            fun print_match ((pat, ty), t) vars =
+            fun print_match ((pat, _), t) vars =
               vars
               |> print_bind is_pseudo_fun some_thm NOBR pat
               |>> (fn p => semicolon [str "val", p, str "=",
                     print_term is_pseudo_fun some_thm vars NOBR t])
             val (ps, vars') = fold_map print_match binds vars;

           | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
               enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
       in
         concat (
           str definer
-          :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)
+          :: print_tyco_expr (tyco, map (ITyVar o fst) vs)
           :: str "="
           :: separate (str "|") (map print_co cos)
         )
       end;
     fun print_def is_pseudo_fun needs_typ definer

               @ str "="
               :: enum "," "{" "}"
                 (map print_super_instance super_instances
                   @ map print_classparam_instance classparam_instances)
               :: str ":"
-              @@ print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
+              @@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
             ))
           end;
     fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
           [print_val_decl print_typscheme (name, vs_ty)]
           ((semicolon o map str) (

             sig_ps
             (Pretty.chunks (ps @ semicolon [p] :: pseudo_ps))
           end
      | print_stmt (ML_Datas [(tyco, (vs, []))]) =
           let
-            val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
+            val ty_p = print_tyco_expr (tyco, map (ITyVar o fst) vs);
           in
             pair
             [concat [str "type", ty_p]]
             (concat [str "datatype", ty_p, str "=", str "EMPTY__"])
           end

 
 (** OCaml serializer **)
 
 fun print_ocaml_stmt tyco_syntax const_syntax reserved is_cons deresolve =
   let
-    fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
-      | print_tyco_expr fxy (tyco, [ty]) =
+    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 fxy (tyco, tys) =
+      | print_tyco_expr (tyco, tys) =
           concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
     and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
-         of NONE => print_tyco_expr fxy (tyco, tys)
+         of NONE => print_tyco_expr (tyco, tys)
           | SOME (_, print) => print print_typ fxy tys)
       | print_typ fxy (ITyVar v) = str ("'" ^ v);
-    fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
+    fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]);
     fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
       (map_filter (fn (v, sort) =>
         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);

           | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
               enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
       in
         concat (
           str definer
-          :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)
+          :: print_tyco_expr (tyco, map (ITyVar o fst) vs)
           :: str "="
           :: separate (str "|") (map print_co cos)
         )
       end;
     fun print_def is_pseudo_fun needs_typ definer

               @ str "="
               @@ brackets [
                 enum_default "()" ";" "{" "}" (map print_super_instance super_instances
                   @ map print_classparam_instance classparam_instances),
                 str ":",
-                print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
+                print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
               ]
             ))
           end;
      fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
           [print_val_decl print_typscheme (name, vs_ty)]

             sig_ps
             (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps))
           end
      | print_stmt (ML_Datas [(tyco, (vs, []))]) =
           let
-            val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
+            val ty_p = print_tyco_expr (tyco, map (ITyVar o fst) vs);
           in
             pair
             [concat [str "type", ty_p]]
             (concat [str "type", ty_p, str "=", str "EMPTY__"])
           end