dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
authorhaftmann
Wed Oct 14 11:56:44 2009 +0200 (2009-10-14)
changeset 32924d2e9b2dab760
parent 32923 0b92e6359bc4
child 32925 980f5aa0d2d7
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_printer.ML
     1.1 --- a/src/Tools/Code/code_haskell.ML	Tue Oct 13 14:57:53 2009 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Wed Oct 14 11:56:44 2009 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4  (** Haskell serializer **)
     1.5  
     1.6  fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
     1.7 -    init_syms deresolve contr_classparam_typs deriving_show =
     1.8 +    reserved deresolve contr_classparam_typs deriving_show =
     1.9    let
    1.10      val deresolve_base = Long_Name.base_name o deresolve;
    1.11      fun class_name class = case syntax_class class
    1.12 @@ -34,18 +34,18 @@
    1.13       of [] => []
    1.14        | classbinds => Pretty.enum "," "(" ")" (
    1.15            map (fn (v, class) =>
    1.16 -            str (class_name class ^ " " ^ Code_Printer.lookup_var tyvars v)) classbinds)
    1.17 +            str (class_name class ^ " " ^ lookup_var tyvars v)) classbinds)
    1.18            @@ str " => ";
    1.19      fun pr_typforall tyvars vs = case map fst vs
    1.20       of [] => []
    1.21        | vnames => str "forall " :: Pretty.breaks
    1.22 -          (map (str o Code_Printer.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
    1.23 +          (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
    1.24      fun pr_tycoexpr tyvars fxy (tyco, tys) =
    1.25        brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
    1.26      and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
    1.27           of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
    1.28            | SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
    1.29 -      | pr_typ tyvars fxy (ITyVar v) = (str o Code_Printer.lookup_var tyvars) v;
    1.30 +      | pr_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
    1.31      fun pr_typdecl tyvars (vs, tycoexpr) =
    1.32        Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
    1.33      fun pr_typscheme tyvars (vs, ty) =
    1.34 @@ -63,7 +63,7 @@
    1.35        | pr_term tyvars thm vars fxy (IVar NONE) =
    1.36            str "_"
    1.37        | pr_term tyvars thm vars fxy (IVar (SOME v)) =
    1.38 -          (str o Code_Printer.lookup_var vars) v
    1.39 +          (str o lookup_var vars) v
    1.40        | pr_term tyvars thm vars fxy (t as _ `|=> _) =
    1.41            let
    1.42              val (binds, t') = Code_Thingol.unfold_pat_abs t;
    1.43 @@ -118,7 +118,7 @@
    1.44            (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
    1.45      fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
    1.46            let
    1.47 -            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
    1.48 +            val tyvars = intro_vars (map fst vs) reserved;
    1.49              val n = (length o fst o Code_Thingol.unfold_fun) ty;
    1.50            in
    1.51              Pretty.chunks [
    1.52 @@ -141,14 +141,14 @@
    1.53        | pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
    1.54            let
    1.55              val eqs = filter (snd o snd) raw_eqs;
    1.56 -            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
    1.57 +            val tyvars = intro_vars (map fst vs) reserved;
    1.58              fun pr_eq ((ts, t), (thm, _)) =
    1.59                let
    1.60                  val consts = fold Code_Thingol.add_constnames (t :: ts) [];
    1.61 -                val vars = init_syms
    1.62 -                  |> Code_Printer.intro_base_names
    1.63 +                val vars = reserved
    1.64 +                  |> intro_base_names
    1.65                        (is_none o syntax_const) deresolve consts
    1.66 -                  |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
    1.67 +                  |> intro_vars ((fold o Code_Thingol.fold_varnames)
    1.68                         (insert (op =)) ts []);
    1.69                in
    1.70                  semicolon (
    1.71 @@ -171,7 +171,7 @@
    1.72            end
    1.73        | pr_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
    1.74            let
    1.75 -            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
    1.76 +            val tyvars = intro_vars (map fst vs) reserved;
    1.77            in
    1.78              semicolon [
    1.79                str "data",
    1.80 @@ -180,7 +180,7 @@
    1.81            end
    1.82        | pr_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) =
    1.83            let
    1.84 -            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
    1.85 +            val tyvars = intro_vars (map fst vs) reserved;
    1.86            in
    1.87              semicolon (
    1.88                str "newtype"
    1.89 @@ -193,7 +193,7 @@
    1.90            end
    1.91        | pr_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
    1.92            let
    1.93 -            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
    1.94 +            val tyvars = intro_vars (map fst vs) reserved;
    1.95              fun pr_co (co, tys) =
    1.96                concat (
    1.97                  (str o deresolve_base) co
    1.98 @@ -211,7 +211,7 @@
    1.99            end
   1.100        | pr_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) =
   1.101            let
   1.102 -            val tyvars = Code_Printer.intro_vars [v] init_syms;
   1.103 +            val tyvars = intro_vars [v] reserved;
   1.104              fun pr_classparam (classparam, ty) =
   1.105                semicolon [
   1.106                  (str o deresolve_base) classparam,
   1.107 @@ -223,7 +223,7 @@
   1.108                Pretty.block [
   1.109                  str "class ",
   1.110                  Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
   1.111 -                str (deresolve_base name ^ " " ^ Code_Printer.lookup_var tyvars v),
   1.112 +                str (deresolve_base name ^ " " ^ lookup_var tyvars v),
   1.113                  str " where {"
   1.114                ],
   1.115                str "};"
   1.116 @@ -231,12 +231,12 @@
   1.117            end
   1.118        | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
   1.119            let
   1.120 -            val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
   1.121 +            val tyvars = intro_vars (map fst vs) reserved;
   1.122              fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
   1.123               of NONE => semicolon [
   1.124                      (str o deresolve_base) classparam,
   1.125                      str "=",
   1.126 -                    pr_app tyvars thm init_syms NOBR (c_inst, [])
   1.127 +                    pr_app tyvars thm reserved NOBR (c_inst, [])
   1.128                    ]
   1.129                | SOME (k, pr) =>
   1.130                    let
   1.131 @@ -245,9 +245,9 @@
   1.132                        then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name;
   1.133                      val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
   1.134                      val (vs, rhs) = (apfst o map) fst (Code_Thingol.unfold_abs proto_rhs);
   1.135 -                    val vars = init_syms
   1.136 -                      |> Code_Printer.intro_vars (the_list const)
   1.137 -                      |> Code_Printer.intro_vars (map_filter I vs);
   1.138 +                    val vars = reserved
   1.139 +                      |> intro_vars (the_list const)
   1.140 +                      |> intro_vars (map_filter I vs);
   1.141                      val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
   1.142                        (*dictionaries are not relevant at this late stage*)
   1.143                    in
   1.144 @@ -271,24 +271,24 @@
   1.145            end;
   1.146    in pr_stmt end;
   1.147  
   1.148 -fun haskell_program_of_program labelled_name module_name module_prefix reserved_names raw_module_alias program =
   1.149 +fun haskell_program_of_program labelled_name module_name module_prefix reserved raw_module_alias program =
   1.150    let
   1.151      val module_alias = if is_some module_name then K module_name else raw_module_alias;
   1.152 -    val reserved_names = Name.make_context reserved_names;
   1.153 -    val mk_name_module = Code_Printer.mk_name_module reserved_names module_prefix module_alias program;
   1.154 +    val reserved = Name.make_context reserved;
   1.155 +    val mk_name_module = mk_name_module reserved module_prefix module_alias program;
   1.156      fun add_stmt (name, (stmt, deps)) =
   1.157        let
   1.158 -        val (module_name, base) = Code_Printer.dest_name name;
   1.159 +        val (module_name, base) = dest_name name;
   1.160          val module_name' = mk_name_module module_name;
   1.161          val mk_name_stmt = yield_singleton Name.variants;
   1.162          fun add_fun upper (nsp_fun, nsp_typ) =
   1.163            let
   1.164              val (base', nsp_fun') =
   1.165 -              mk_name_stmt (if upper then Code_Printer.first_upper base else base) nsp_fun
   1.166 +              mk_name_stmt (if upper then first_upper base else base) nsp_fun
   1.167            in (base', (nsp_fun', nsp_typ)) end;
   1.168          fun add_typ (nsp_fun, nsp_typ) =
   1.169            let
   1.170 -            val (base', nsp_typ') = mk_name_stmt (Code_Printer.first_upper base) nsp_typ
   1.171 +            val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ
   1.172            in (base', (nsp_fun, nsp_typ')) end;
   1.173          val add_name = case stmt
   1.174           of Code_Thingol.Fun _ => add_fun false
   1.175 @@ -306,7 +306,7 @@
   1.176                cons (name, (Long_Name.append module_name' base', NONE))
   1.177            | _ => cons (name, (Long_Name.append module_name' base', SOME stmt));
   1.178        in
   1.179 -        Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names))))
   1.180 +        Symtab.map_default (module_name', ([], ([], (reserved, reserved))))
   1.181                (apfst (fold (insert (op = : string * string -> bool)) deps))
   1.182          #> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name'))
   1.183          #-> (fn (base', names) =>
   1.184 @@ -317,19 +317,19 @@
   1.185        (Graph.get_node program name, Graph.imm_succs program name))
   1.186        (Graph.strong_conn program |> flat)) Symtab.empty;
   1.187      fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the
   1.188 -      o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Printer.dest_name) name))) name
   1.189 +      o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name
   1.190        handle Option => error ("Unknown statement name: " ^ labelled_name name);
   1.191    in (deresolver, hs_program) end;
   1.192  
   1.193  fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
   1.194 -    raw_reserved_names includes raw_module_alias
   1.195 +    raw_reserved includes raw_module_alias
   1.196      syntax_class syntax_tyco syntax_const program cs destination =
   1.197    let
   1.198      val stmt_names = Code_Target.stmt_names_of_destination destination;
   1.199      val module_name = if null stmt_names then raw_module_name else SOME "Code";
   1.200 -    val reserved_names = fold (insert (op =) o fst) includes raw_reserved_names;
   1.201 +    val reserved = fold (insert (op =) o fst) includes raw_reserved;
   1.202      val (deresolver, hs_program) = haskell_program_of_program labelled_name
   1.203 -      module_name module_prefix reserved_names raw_module_alias program;
   1.204 +      module_name module_prefix reserved raw_module_alias program;
   1.205      val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
   1.206      fun deriving_show tyco =
   1.207        let
   1.208 @@ -343,9 +343,9 @@
   1.209                andalso forall (deriv' tycos) tys
   1.210            | deriv' _ (ITyVar _) = true
   1.211        in deriv [] tyco end;
   1.212 -    val reserved_names = Code_Printer.make_vars reserved_names;
   1.213 +    val reserved = make_vars reserved;
   1.214      fun pr_stmt qualified = pr_haskell_stmt labelled_name
   1.215 -      syntax_class syntax_tyco syntax_const reserved_names
   1.216 +      syntax_class syntax_tyco syntax_const reserved
   1.217        (if qualified then deresolver else Long_Name.base_name o deresolver)
   1.218        contr_classparam_typs
   1.219        (if string_classes then deriving_show else K false);
     2.1 --- a/src/Tools/Code/code_ml.ML	Tue Oct 13 14:57:53 2009 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Wed Oct 14 11:56:44 2009 +0200
     2.3 @@ -45,12 +45,12 @@
     2.4  
     2.5  (** SML serailizer **)
     2.6  
     2.7 -fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
     2.8 +fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved deresolve is_cons =
     2.9    let
    2.10      fun pr_dicts fxy ds =
    2.11        let
    2.12 -        fun pr_dictvar (v, (_, 1)) = Code_Printer.first_upper v ^ "_"
    2.13 -          | pr_dictvar (v, (i, _)) = Code_Printer.first_upper v ^ string_of_int (i+1) ^ "_";
    2.14 +        fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
    2.15 +          | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
    2.16          fun pr_proj [] p =
    2.17                p
    2.18            | pr_proj [p'] p =
    2.19 @@ -88,7 +88,7 @@
    2.20        | pr_term is_closure thm vars fxy (IVar NONE) =
    2.21            str "_"
    2.22        | pr_term is_closure thm vars fxy (IVar (SOME v)) =
    2.23 -          str (Code_Printer.lookup_var vars v)
    2.24 +          str (lookup_var vars v)
    2.25        | pr_term is_closure thm vars fxy (t as t1 `$ t2) =
    2.26            (case Code_Thingol.unfold_const_app t
    2.27             of SOME c_ts => pr_app is_closure thm vars fxy c_ts
    2.28 @@ -176,8 +176,8 @@
    2.29        | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
    2.30            let
    2.31              val consts = Code_Thingol.add_constnames t [];
    2.32 -            val vars = reserved_names
    2.33 -              |> Code_Printer.intro_base_names
    2.34 +            val vars = reserved
    2.35 +              |> intro_base_names
    2.36                    (is_none o syntax_const) deresolve consts;
    2.37            in
    2.38              concat [
    2.39 @@ -199,10 +199,10 @@
    2.40                  fun pr_eq definer ((ts, t), (thm, _)) =
    2.41                    let
    2.42                      val consts = fold Code_Thingol.add_constnames (t :: ts) [];
    2.43 -                    val vars = reserved_names
    2.44 -                      |> Code_Printer.intro_base_names
    2.45 +                    val vars = reserved
    2.46 +                      |> intro_base_names
    2.47                             (is_none o syntax_const) deresolve consts
    2.48 -                      |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
    2.49 +                      |> intro_vars ((fold o Code_Thingol.fold_varnames)
    2.50                             (insert (op =)) ts []);
    2.51                    in
    2.52                      concat (
    2.53 @@ -260,7 +260,7 @@
    2.54            in Pretty.chunks (ps @| Pretty.block ([p, str ";"])) end
    2.55       | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
    2.56            let
    2.57 -            val w = Code_Printer.first_upper v ^ "_";
    2.58 +            val w = first_upper v ^ "_";
    2.59              fun pr_superclass_field (class, classrel) =
    2.60                (concat o map str) [
    2.61                  deresolve classrel, ":", "'" ^ v, deresolve class
    2.62 @@ -313,7 +313,7 @@
    2.63                concat [
    2.64                  (str o Long_Name.base_name o deresolve) classparam,
    2.65                  str "=",
    2.66 -                pr_app (K false) thm reserved_names NOBR (c_inst, [])
    2.67 +                pr_app (K false) thm reserved NOBR (c_inst, [])
    2.68                ];
    2.69            in
    2.70              semicolon ([
    2.71 @@ -352,12 +352,12 @@
    2.72  
    2.73  (** OCaml serializer **)
    2.74  
    2.75 -fun pr_ocaml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
    2.76 +fun pr_ocaml_stmt labelled_name syntax_tyco syntax_const reserved deresolve is_cons =
    2.77    let
    2.78      fun pr_dicts fxy ds =
    2.79        let
    2.80 -        fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Printer.first_upper v
    2.81 -          | pr_dictvar (v, (i, _)) = "_" ^ Code_Printer.first_upper v ^ string_of_int (i+1);
    2.82 +        fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
    2.83 +          | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
    2.84          fun pr_proj ps p =
    2.85            fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
    2.86          fun pr_dict fxy (DictConst (inst, dss)) =
    2.87 @@ -391,7 +391,7 @@
    2.88        | pr_term is_closure thm vars fxy (IVar NONE) =
    2.89            str "_"
    2.90        | pr_term is_closure thm vars fxy (IVar (SOME v)) =
    2.91 -          str (Code_Printer.lookup_var vars v)
    2.92 +          str (lookup_var vars v)
    2.93        | pr_term is_closure thm vars fxy (t as t1 `$ t2) =
    2.94            (case Code_Thingol.unfold_const_app t
    2.95             of SOME c_ts => pr_app is_closure thm vars fxy c_ts
    2.96 @@ -469,8 +469,8 @@
    2.97        | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) =
    2.98            let
    2.99              val consts = Code_Thingol.add_constnames t [];
   2.100 -            val vars = reserved_names
   2.101 -              |> Code_Printer.intro_base_names
   2.102 +            val vars = reserved
   2.103 +              |> intro_base_names
   2.104                    (is_none o syntax_const) deresolve consts;
   2.105            in
   2.106              concat [
   2.107 @@ -487,10 +487,10 @@
   2.108              fun pr_eq ((ts, t), (thm, _)) =
   2.109                let
   2.110                  val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   2.111 -                val vars = reserved_names
   2.112 -                  |> Code_Printer.intro_base_names
   2.113 +                val vars = reserved
   2.114 +                  |> intro_base_names
   2.115                        (is_none o syntax_const) deresolve consts
   2.116 -                  |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
   2.117 +                  |> intro_vars ((fold o Code_Thingol.fold_varnames)
   2.118                        (insert (op =)) ts []);
   2.119                in concat [
   2.120                  (Pretty.block o Pretty.commas)
   2.121 @@ -501,10 +501,10 @@
   2.122              fun pr_eqs is_pseudo [((ts, t), (thm, _))] =
   2.123                    let
   2.124                      val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   2.125 -                    val vars = reserved_names
   2.126 -                      |> Code_Printer.intro_base_names
   2.127 +                    val vars = reserved
   2.128 +                      |> intro_base_names
   2.129                            (is_none o syntax_const) deresolve consts
   2.130 -                      |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
   2.131 +                      |> intro_vars ((fold o Code_Thingol.fold_varnames)
   2.132                            (insert (op =)) ts []);
   2.133                    in
   2.134                      concat (
   2.135 @@ -527,10 +527,10 @@
   2.136                | pr_eqs _ (eqs as eq :: eqs') =
   2.137                    let
   2.138                      val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
   2.139 -                    val vars = reserved_names
   2.140 -                  |> Code_Printer.intro_base_names
   2.141 +                    val vars = reserved
   2.142 +                      |> intro_base_names
   2.143                        (is_none o syntax_const) deresolve consts;
   2.144 -                    val dummy_parms = (map str o Code_Printer.aux_params vars o map (fst o fst)) eqs;
   2.145 +                    val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
   2.146                    in
   2.147                      Pretty.block (
   2.148                        Pretty.breaks dummy_parms
   2.149 @@ -595,7 +595,7 @@
   2.150            in Pretty.chunks (ps @| Pretty.block ([p, str ";;"])) end
   2.151       | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
   2.152            let
   2.153 -            val w = "_" ^ Code_Printer.first_upper v;
   2.154 +            val w = "_" ^ first_upper v;
   2.155              fun pr_superclass_field (class, classrel) =
   2.156                (concat o map str) [
   2.157                  deresolve classrel, ":", "'" ^ v, deresolve class
   2.158 @@ -636,7 +636,7 @@
   2.159                concat [
   2.160                  (str o deresolve) classparam,
   2.161                  str "=",
   2.162 -                pr_app (K false) thm reserved_names NOBR (c_inst, [])
   2.163 +                pr_app (K false) thm reserved NOBR (c_inst, [])
   2.164                ];
   2.165            in
   2.166              concat (
   2.167 @@ -705,11 +705,11 @@
   2.168  
   2.169  in
   2.170  
   2.171 -fun ml_node_of_program labelled_name module_name reserved_names raw_module_alias program =
   2.172 +fun ml_node_of_program labelled_name module_name reserved raw_module_alias program =
   2.173    let
   2.174      val module_alias = if is_some module_name then K module_name else raw_module_alias;
   2.175 -    val reserved_names = Name.make_context reserved_names;
   2.176 -    val empty_module = ((reserved_names, reserved_names), Graph.empty);
   2.177 +    val reserved = Name.make_context reserved;
   2.178 +    val empty_module = ((reserved, reserved), Graph.empty);
   2.179      fun map_node [] f = f
   2.180        | map_node (m::ms) f =
   2.181            Graph.default_node (m, Module (m, empty_module))
   2.182 @@ -737,11 +737,11 @@
   2.183        let
   2.184          val (x, nsp_typ') = f nsp_typ
   2.185        in (x, (nsp_fun, nsp_typ')) end;
   2.186 -    val mk_name_module = Code_Printer.mk_name_module reserved_names NONE module_alias program;
   2.187 +    val mk_name_module = mk_name_module reserved NONE module_alias program;
   2.188      fun mk_name_stmt upper name nsp =
   2.189        let
   2.190 -        val (_, base) = Code_Printer.dest_name name;
   2.191 -        val base' = if upper then Code_Printer.first_upper base else base;
   2.192 +        val (_, base) = dest_name name;
   2.193 +        val base' = if upper then first_upper base else base;
   2.194          val ([base''], nsp') = Name.variants [base'] nsp;
   2.195        in (base'', nsp') end;
   2.196      fun rearrange_fun name (tysm as (vs, ty), raw_eqs) =
   2.197 @@ -824,7 +824,7 @@
   2.198            []
   2.199            |> fold (fold (insert (op =)) o Graph.imm_succs program) names
   2.200            |> subtract (op =) names;
   2.201 -        val (module_names, _) = (split_list o map Code_Printer.dest_name) names;
   2.202 +        val (module_names, _) = (split_list o map dest_name) names;
   2.203          val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
   2.204            handle Empty =>
   2.205              error ("Different namespace prefixes for mutual dependencies:\n"
   2.206 @@ -834,7 +834,7 @@
   2.207          val module_name_path = Long_Name.explode module_name;
   2.208          fun add_dep name name' =
   2.209            let
   2.210 -            val module_name' = (mk_name_module o fst o Code_Printer.dest_name) name';
   2.211 +            val module_name' = (mk_name_module o fst o dest_name) name';
   2.212            in if module_name = module_name' then
   2.213              map_node module_name_path (Graph.add_edge (name, name'))
   2.214            else let
   2.215 @@ -862,7 +862,7 @@
   2.216            (rev (Graph.strong_conn program)));
   2.217      fun deresolver prefix name = 
   2.218        let
   2.219 -        val module_name = (fst o Code_Printer.dest_name) name;
   2.220 +        val module_name = (fst o dest_name) name;
   2.221          val module_name' = (Long_Name.explode o mk_name_module) module_name;
   2.222          val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
   2.223          val stmt_name =
   2.224 @@ -877,7 +877,7 @@
   2.225          error ("Unknown statement name: " ^ labelled_name name);
   2.226    in (deresolver, nodes) end;
   2.227  
   2.228 -fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
   2.229 +fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved includes raw_module_alias
   2.230    _ syntax_tyco syntax_const program stmt_names destination =
   2.231    let
   2.232      val is_cons = Code_Thingol.is_cons program;
   2.233 @@ -885,15 +885,15 @@
   2.234      val is_present = not (null present_stmt_names);
   2.235      val module_name = if is_present then SOME "Code" else raw_module_name;
   2.236      val (deresolver, nodes) = ml_node_of_program labelled_name module_name
   2.237 -      reserved_names raw_module_alias program;
   2.238 -    val reserved_names = Code_Printer.make_vars reserved_names;
   2.239 +      reserved raw_module_alias program;
   2.240 +    val reserved = make_vars reserved;
   2.241      fun pr_node prefix (Dummy _) =
   2.242            NONE
   2.243        | pr_node prefix (Stmt (_, stmt)) = if is_present andalso
   2.244            (null o filter (member (op =) present_stmt_names) o stmt_names_of) stmt
   2.245            then NONE
   2.246            else SOME
   2.247 -            (pr_stmt labelled_name syntax_tyco syntax_const reserved_names
   2.248 +            (pr_stmt labelled_name syntax_tyco syntax_const reserved
   2.249                (deresolver prefix) is_cons stmt)
   2.250        | pr_node prefix (Module (module_name, (_, nodes))) =
   2.251            separate (str "")
     3.1 --- a/src/Tools/Code/code_printer.ML	Tue Oct 13 14:57:53 2009 +0200
     3.2 +++ b/src/Tools/Code/code_printer.ML	Wed Oct 14 11:56:44 2009 +0200
     3.3 @@ -316,13 +316,13 @@
     3.4  val dest_name =
     3.5    apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
     3.6  
     3.7 -fun mk_name_module reserved_names module_prefix module_alias program =
     3.8 +fun mk_name_module reserved module_prefix module_alias program =
     3.9    let
    3.10      fun mk_alias name = case module_alias name
    3.11       of SOME name' => name'
    3.12        | NONE => name
    3.13            |> Long_Name.explode
    3.14 -          |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
    3.15 +          |> map (fn name => (the_single o fst) (Name.variants [name] reserved))
    3.16            |> Long_Name.implode;
    3.17      fun mk_prefix name = case module_prefix
    3.18       of SOME module_prefix => Long_Name.append module_prefix name