less clumsy namespace
authorhaftmann
Sat Jan 25 23:50:49 2014 +0100 (2014-01-25)
changeset 551500940309ed8f1
parent 55149 626d8f08d479
child 55151 f331472f1027
less clumsy namespace
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_namespace.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_symbol.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Tools/Code/code_haskell.ML	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -25,6 +25,7 @@
     1.4  val language_params =
     1.5    space_implode " " (map (prefix "-X") language_extensions);
     1.6  
     1.7 +open Basic_Code_Symbol;
     1.8  open Basic_Code_Thingol;
     1.9  open Code_Printer;
    1.10  
    1.11 @@ -37,9 +38,9 @@
    1.12  fun print_haskell_stmt class_syntax tyco_syntax const_syntax
    1.13      reserved deresolve deriving_show =
    1.14    let
    1.15 -    val deresolve_const = deresolve o Code_Symbol.Constant;
    1.16 -    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
    1.17 -    val deresolve_class = deresolve o Code_Symbol.Type_Class;
    1.18 +    val deresolve_const = deresolve o Constant;
    1.19 +    val deresolve_tyco = deresolve o Type_Constructor;
    1.20 +    val deresolve_class = deresolve o Type_Class;
    1.21      fun class_name class = case class_syntax class
    1.22       of NONE => deresolve_class class
    1.23        | SOME class => class;
    1.24 @@ -84,7 +85,7 @@
    1.25            in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
    1.26        | print_term tyvars some_thm vars fxy (ICase case_expr) =
    1.27            (case Code_Thingol.unfold_const_app (#primitive case_expr)
    1.28 -           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
    1.29 +           of SOME (app as ({ sym = Constant const, ... }, _)) =>
    1.30                  if is_none (const_syntax const)
    1.31                  then print_case tyvars some_thm vars fxy case_expr
    1.32                  else print_app tyvars some_thm vars fxy app
    1.33 @@ -126,7 +127,7 @@
    1.34              (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
    1.35              (map print_select clauses)
    1.36            end;
    1.37 -    fun print_stmt (Code_Symbol.Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
    1.38 +    fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
    1.39            let
    1.40              val tyvars = intro_vars (map fst vs) reserved;
    1.41              fun print_err n =
    1.42 @@ -163,7 +164,7 @@
    1.43                  | eqs => map print_eqn eqs)
    1.44              )
    1.45            end
    1.46 -      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) =
    1.47 +      | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) =
    1.48            let
    1.49              val tyvars = intro_vars vs reserved;
    1.50            in
    1.51 @@ -172,7 +173,7 @@
    1.52                print_typdecl tyvars (deresolve_tyco tyco, vs)
    1.53              ]
    1.54            end
    1.55 -      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) =
    1.56 +      | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) =
    1.57            let
    1.58              val tyvars = intro_vars vs reserved;
    1.59            in
    1.60 @@ -185,7 +186,7 @@
    1.61                :: (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
    1.62              )
    1.63            end
    1.64 -      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
    1.65 +      | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
    1.66            let
    1.67              val tyvars = intro_vars vs reserved;
    1.68              fun print_co ((co, _), tys) =
    1.69 @@ -203,7 +204,7 @@
    1.70                @ (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
    1.71              )
    1.72            end
    1.73 -      | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
    1.74 +      | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
    1.75            let
    1.76              val tyvars = intro_vars [v] reserved;
    1.77              fun print_classparam (classparam, ty) =
    1.78 @@ -239,14 +240,14 @@
    1.79                      ]
    1.80                  | SOME k =>
    1.81                      let
    1.82 -                      val { sym = Code_Symbol.Constant c, dom, range, ... } = const;
    1.83 +                      val { sym = Constant c, dom, range, ... } = const;
    1.84                        val (vs, rhs) = (apfst o map) fst
    1.85                          (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
    1.86                        val s = if (is_some o const_syntax) c
    1.87                          then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
    1.88                        val vars = reserved
    1.89                          |> intro_vars (map_filter I (s :: vs));
    1.90 -                      val lhs = IConst { sym = Code_Symbol.Constant classparam, typargs = [],
    1.91 +                      val lhs = IConst { sym = Constant classparam, typargs = [],
    1.92                          dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
    1.93                          (*dictionaries are not relevant at this late stage,
    1.94                            and these consts never need type annotations for disambiguation *)
    1.95 @@ -340,7 +341,7 @@
    1.96        let
    1.97          fun deriv _ "fun" = false
    1.98            | deriv tycos tyco = member (op =) tycos tyco
    1.99 -              orelse case try (Code_Symbol.Graph.get_node program) (Code_Symbol.Type_Constructor tyco)
   1.100 +              orelse case try (Code_Symbol.Graph.get_node program) (Type_Constructor tyco)
   1.101                  of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
   1.102                      (maps snd cs)
   1.103                   | NONE => true
   1.104 @@ -432,7 +433,7 @@
   1.105       of SOME ((pat, ty), t') =>
   1.106            SOME ((SOME ((pat, ty), true), t1), t')
   1.107        | NONE => NONE;
   1.108 -    fun dest_monad (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
   1.109 +    fun dest_monad (IConst { sym = Constant c, ... } `$ t1 `$ t2) =
   1.110            if c = c_bind then dest_bind t1 t2
   1.111            else NONE
   1.112        | dest_monad t = case Code_Thingol.split_let t
   1.113 @@ -467,7 +468,7 @@
   1.114    in
   1.115      if target = target' then
   1.116        thy
   1.117 -      |> Code_Target.set_printings (Code_Symbol.Constant (c_bind, [(target,
   1.118 +      |> Code_Target.set_printings (Constant (c_bind, [(target,
   1.119          SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))]))
   1.120      else error "Only Haskell target allows for monad syntax"
   1.121    end;
   1.122 @@ -487,7 +488,7 @@
   1.123          make_command = fn module_name =>
   1.124            "\"$ISABELLE_GHC\" " ^ language_params  ^ " -odir build -hidir build -stubdir build -e \"\" " ^
   1.125              module_name ^ ".hs" } })
   1.126 -  #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
   1.127 +  #> Code_Target.set_printings (Type_Constructor ("fun",
   1.128      [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   1.129        brackify_infix (1, R) fxy (
   1.130          print_typ (INFX (1, X)) ty1,
     2.1 --- a/src/Tools/Code/code_ml.ML	Sat Jan 25 23:50:49 2014 +0100
     2.2 +++ b/src/Tools/Code/code_ml.ML	Sat Jan 25 23:50:49 2014 +0100
     2.3 @@ -14,6 +14,7 @@
     2.4  structure Code_ML : CODE_ML =
     2.5  struct
     2.6  
     2.7 +open Basic_Code_Symbol;
     2.8  open Basic_Code_Thingol;
     2.9  open Code_Printer;
    2.10  
    2.11 @@ -36,7 +37,7 @@
    2.12  datatype ml_stmt =
    2.13      ML_Exc of string * (typscheme * int)
    2.14    | ML_Val of ml_binding
    2.15 -  | ML_Funs of ml_binding list * Code_Symbol.symbol list
    2.16 +  | ML_Funs of ml_binding list * Code_Symbol.T list
    2.17    | ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list
    2.18    | ML_Class of string * (vname * ((class * class) list * (string * itype) list));
    2.19  
    2.20 @@ -53,21 +54,21 @@
    2.21  
    2.22  fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
    2.23    let
    2.24 -    val deresolve_const = deresolve o Code_Symbol.Constant;
    2.25 -    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
    2.26 -    val deresolve_class = deresolve o Code_Symbol.Type_Class;
    2.27 -    val deresolve_classrel = deresolve o Code_Symbol.Class_Relation;
    2.28 -    val deresolve_inst = deresolve o Code_Symbol.Class_Instance;
    2.29 +    val deresolve_const = deresolve o Constant;
    2.30 +    val deresolve_tyco = deresolve o Type_Constructor;
    2.31 +    val deresolve_class = deresolve o Type_Class;
    2.32 +    val deresolve_classrel = deresolve o Class_Relation;
    2.33 +    val deresolve_inst = deresolve o Class_Instance;
    2.34      fun print_tyco_expr (sym, []) = (str o deresolve) sym
    2.35        | print_tyco_expr (sym, [ty]) =
    2.36            concat [print_typ BR ty, (str o deresolve) sym]
    2.37        | print_tyco_expr (sym, tys) =
    2.38            concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
    2.39      and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
    2.40 -         of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys)
    2.41 +         of NONE => print_tyco_expr (Type_Constructor tyco, tys)
    2.42            | SOME (_, print) => print print_typ fxy tys)
    2.43        | print_typ fxy (ITyVar v) = str ("'" ^ v);
    2.44 -    fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]);
    2.45 +    fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
    2.46      fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
    2.47        (map_filter (fn (v, sort) =>
    2.48          (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
    2.49 @@ -81,7 +82,7 @@
    2.50        print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)
    2.51      and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
    2.52            ((str o deresolve_inst) inst ::
    2.53 -            (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
    2.54 +            (if is_pseudo_fun (Class_Instance inst) then [str "()"]
    2.55              else map_filter (print_dicts is_pseudo_fun BR) dss))
    2.56        | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
    2.57            [str (if k = 1 then first_upper v ^ "_"
    2.58 @@ -110,7 +111,7 @@
    2.59            in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
    2.60        | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
    2.61            (case Code_Thingol.unfold_const_app (#primitive case_expr)
    2.62 -           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
    2.63 +           of SOME (app as ({ sym = Constant const, ... }, _)) =>
    2.64                  if is_none (const_syntax const)
    2.65                  then print_case is_pseudo_fun some_thm vars fxy case_expr
    2.66                  else print_app is_pseudo_fun some_thm vars fxy app
    2.67 @@ -174,7 +175,7 @@
    2.68        in
    2.69          concat (
    2.70            str definer
    2.71 -          :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
    2.72 +          :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
    2.73            :: str "="
    2.74            :: separate (str "|") (map print_co cos)
    2.75          )
    2.76 @@ -195,7 +196,7 @@
    2.77                in
    2.78                  concat (
    2.79                    prolog
    2.80 -                  :: (if is_pseudo_fun (Code_Symbol.Constant const) then [str "()"]
    2.81 +                  :: (if is_pseudo_fun (Constant const) then [str "()"]
    2.82                        else print_dict_args vs
    2.83                          @ map (print_term is_pseudo_fun some_thm vars BR) ts)
    2.84                    @ str "="
    2.85 @@ -205,7 +206,7 @@
    2.86              val shift = if null eqs then I else
    2.87                map (Pretty.block o single o Pretty.block o single);
    2.88            in pair
    2.89 -            (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
    2.90 +            (print_val_decl print_typscheme (Constant const, vs_ty))
    2.91              ((Pretty.block o Pretty.fbreaks o shift) (
    2.92                print_eqn definer eq
    2.93                :: map (print_eqn "|") eqs
    2.94 @@ -228,11 +229,11 @@
    2.95                ];
    2.96            in pair
    2.97              (print_val_decl print_dicttypscheme
    2.98 -              (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
    2.99 +              (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   2.100              (concat (
   2.101                str definer
   2.102                :: (str o deresolve_inst) inst
   2.103 -              :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
   2.104 +              :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
   2.105                    else print_dict_args vs)
   2.106                @ str "="
   2.107                :: enum "," "{" "}"
   2.108 @@ -243,7 +244,7 @@
   2.109              ))
   2.110            end;
   2.111      fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
   2.112 -          [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
   2.113 +          [print_val_decl print_typscheme (Constant const, vs_ty)]
   2.114            ((semicolon o map str) (
   2.115              (if n = 0 then "val" else "fun")
   2.116              :: deresolve_const const
   2.117 @@ -279,7 +280,7 @@
   2.118            end
   2.119       | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   2.120            let
   2.121 -            val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
   2.122 +            val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
   2.123            in
   2.124              pair
   2.125              [concat [str "type", ty_p]]
   2.126 @@ -301,7 +302,7 @@
   2.127                (map str ["val", s, "=", "#" ^ s, ":"] @| p);
   2.128              fun print_super_class_decl (classrel as (_, super_class)) =
   2.129                print_val_decl print_dicttypscheme
   2.130 -                (Code_Symbol.Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
   2.131 +                (Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
   2.132              fun print_super_class_field (classrel as (_, super_class)) =
   2.133                print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
   2.134              fun print_super_class_proj (classrel as (_, super_class)) =
   2.135 @@ -309,7 +310,7 @@
   2.136                  (print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));
   2.137              fun print_classparam_decl (classparam, ty) =
   2.138                print_val_decl print_typscheme
   2.139 -                (Code_Symbol.Constant classparam, ([(v, [class])], ty));
   2.140 +                (Constant classparam, ([(v, [class])], ty));
   2.141              fun print_classparam_field (classparam, ty) =
   2.142                print_field (deresolve_const classparam) (print_typ NOBR ty);
   2.143              fun print_classparam_proj (classparam, ty) =
   2.144 @@ -359,21 +360,21 @@
   2.145  
   2.146  fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   2.147    let
   2.148 -    val deresolve_const = deresolve o Code_Symbol.Constant;
   2.149 -    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
   2.150 -    val deresolve_class = deresolve o Code_Symbol.Type_Class;
   2.151 -    val deresolve_classrel = deresolve o Code_Symbol.Class_Relation;
   2.152 -    val deresolve_inst = deresolve o Code_Symbol.Class_Instance;
   2.153 +    val deresolve_const = deresolve o Constant;
   2.154 +    val deresolve_tyco = deresolve o Type_Constructor;
   2.155 +    val deresolve_class = deresolve o Type_Class;
   2.156 +    val deresolve_classrel = deresolve o Class_Relation;
   2.157 +    val deresolve_inst = deresolve o Class_Instance;
   2.158      fun print_tyco_expr (sym, []) = (str o deresolve) sym
   2.159        | print_tyco_expr (sym, [ty]) =
   2.160            concat [print_typ BR ty, (str o deresolve) sym]
   2.161        | print_tyco_expr (sym, tys) =
   2.162            concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
   2.163      and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
   2.164 -         of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys)
   2.165 +         of NONE => print_tyco_expr (Type_Constructor tyco, tys)
   2.166            | SOME (_, print) => print print_typ fxy tys)
   2.167        | print_typ fxy (ITyVar v) = str ("'" ^ v);
   2.168 -    fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]);
   2.169 +    fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
   2.170      fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
   2.171        (map_filter (fn (v, sort) =>
   2.172          (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
   2.173 @@ -386,7 +387,7 @@
   2.174        |> print_classrels classrels
   2.175      and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
   2.176            brackify BR ((str o deresolve_inst) inst ::
   2.177 -            (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
   2.178 +            (if is_pseudo_fun (Class_Instance inst) then [str "()"]
   2.179              else map_filter (print_dicts is_pseudo_fun BR) dss))
   2.180        | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
   2.181            str (if k = 1 then "_" ^ first_upper v
   2.182 @@ -412,7 +413,7 @@
   2.183            in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
   2.184        | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
   2.185            (case Code_Thingol.unfold_const_app (#primitive case_expr)
   2.186 -           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
   2.187 +           of SOME (app as ({ sym = Constant const, ... }, _)) =>
   2.188                  if is_none (const_syntax const)
   2.189                  then print_case is_pseudo_fun some_thm vars fxy case_expr
   2.190                  else print_app is_pseudo_fun some_thm vars fxy app
   2.191 @@ -471,7 +472,7 @@
   2.192        in
   2.193          concat (
   2.194            str definer
   2.195 -          :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
   2.196 +          :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
   2.197            :: str "="
   2.198            :: separate (str "|") (map print_co cos)
   2.199          )
   2.200 @@ -544,11 +545,11 @@
   2.201                concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
   2.202                  else (concat o map str) [definer, deresolve_const const];
   2.203            in pair
   2.204 -            (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
   2.205 +            (print_val_decl print_typscheme (Constant const, vs_ty))
   2.206              (concat (
   2.207                prolog
   2.208                :: print_dict_args vs
   2.209 -              @| print_eqns (is_pseudo_fun (Code_Symbol.Constant const)) eqs
   2.210 +              @| print_eqns (is_pseudo_fun (Constant const)) eqs
   2.211              ))
   2.212            end
   2.213        | print_def is_pseudo_fun _ definer
   2.214 @@ -568,11 +569,11 @@
   2.215                ];
   2.216            in pair
   2.217              (print_val_decl print_dicttypscheme
   2.218 -              (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   2.219 +              (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   2.220              (concat (
   2.221                str definer
   2.222                :: (str o deresolve_inst) inst
   2.223 -              :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
   2.224 +              :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
   2.225                    else print_dict_args vs)
   2.226                @ str "="
   2.227                @@ brackets [
   2.228 @@ -584,7 +585,7 @@
   2.229              ))
   2.230            end;
   2.231       fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
   2.232 -          [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
   2.233 +          [print_val_decl print_typscheme (Constant const, vs_ty)]
   2.234            ((doublesemicolon o map str) (
   2.235              "let"
   2.236              :: deresolve_const const
   2.237 @@ -619,7 +620,7 @@
   2.238            end
   2.239       | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   2.240            let
   2.241 -            val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
   2.242 +            val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
   2.243            in
   2.244              pair
   2.245              [concat [str "type", ty_p]]
   2.246 @@ -641,7 +642,7 @@
   2.247                print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
   2.248              fun print_classparam_decl (classparam, ty) =
   2.249                print_val_decl print_typscheme
   2.250 -                (Code_Symbol.Constant classparam, ([(v, [class])], ty));
   2.251 +                (Constant classparam, ([(v, [class])], ty));
   2.252              fun print_classparam_field (classparam, ty) =
   2.253                print_field (deresolve_const classparam) (print_typ NOBR ty);
   2.254              val w = "_" ^ first_upper v;
   2.255 @@ -724,7 +725,7 @@
   2.256        | namify_stmt (Code_Thingol.Classrel _) = namify_const false
   2.257        | namify_stmt (Code_Thingol.Classparam _) = namify_const false
   2.258        | namify_stmt (Code_Thingol.Classinst _) = namify_const false;
   2.259 -    fun ml_binding_of_stmt (sym as Code_Symbol.Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
   2.260 +    fun ml_binding_of_stmt (sym as Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
   2.261            let
   2.262              val eqs = filter (snd o snd) raw_eqs;
   2.263              val (eqs', some_sym) = if null (filter_out (null o snd) vs) then case eqs
   2.264 @@ -734,7 +735,7 @@
   2.265                  | _ => (eqs, NONE)
   2.266                else (eqs, NONE)
   2.267            in (ML_Function (const, (tysm, eqs')), some_sym) end
   2.268 -      | ml_binding_of_stmt (sym as Code_Symbol.Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
   2.269 +      | ml_binding_of_stmt (sym as Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
   2.270            (ML_Instance (inst, stmt), if forall (null o snd) vs then SOME (sym, false) else NONE)
   2.271        | ml_binding_of_stmt (sym, _) =
   2.272            error ("Binding block containing illegal statement: " ^ 
   2.273 @@ -755,10 +756,10 @@
   2.274        (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
   2.275      fun modify_datatypes stmts = single (SOME
   2.276        (ML_Datas (map_filter
   2.277 -        (fn (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
   2.278 +        (fn (Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
   2.279      fun modify_class stmts = single (SOME
   2.280        (ML_Class (the_single (map_filter
   2.281 -        (fn (Code_Symbol.Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
   2.282 +        (fn (Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
   2.283      fun modify_stmts ([stmt as (_, stmt' as Code_Thingol.Fun _)]) =
   2.284            if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
   2.285        | modify_stmts ((stmts as (_, Code_Thingol.Fun _) :: _)) =
   2.286 @@ -850,7 +851,7 @@
   2.287        check = { env_var = "ISABELLE_OCAML",
   2.288          make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   2.289          make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
   2.290 -  #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
   2.291 +  #> Code_Target.set_printings (Type_Constructor ("fun",
   2.292      [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
   2.293    #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   2.294    #> fold (Code_Target.add_reserved target_SML)
     3.1 --- a/src/Tools/Code/code_namespace.ML	Sat Jan 25 23:50:49 2014 +0100
     3.2 +++ b/src/Tools/Code/code_namespace.ML	Sat Jan 25 23:50:49 2014 +0100
     3.3 @@ -13,7 +13,7 @@
     3.4      namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a,
     3.5      modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option }
     3.6        -> Code_Thingol.program
     3.7 -      -> { deresolver: string -> Code_Symbol.symbol -> string,
     3.8 +      -> { deresolver: string -> Code_Symbol.T -> string,
     3.9             flat_program: flat_program }
    3.10  
    3.11    datatype ('a, 'b) node =
    3.12 @@ -26,13 +26,13 @@
    3.13      reserved: Name.context, identifiers: Code_Target.identifier_data,
    3.14      empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
    3.15      namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
    3.16 -    cyclic_modules: bool, empty_data: 'b, memorize_data: Code_Symbol.symbol -> 'b -> 'b,
    3.17 -    modify_stmts: (Code_Symbol.symbol * Code_Thingol.stmt) list -> 'a option list }
    3.18 +    cyclic_modules: bool, empty_data: 'b, memorize_data: Code_Symbol.T -> 'b -> 'b,
    3.19 +    modify_stmts: (Code_Symbol.T * Code_Thingol.stmt) list -> 'a option list }
    3.20        -> Code_Thingol.program
    3.21 -      -> { deresolver: string list -> Code_Symbol.symbol -> string,
    3.22 +      -> { deresolver: string list -> Code_Symbol.T -> string,
    3.23             hierarchical_program: ('a, 'b) hierarchical_program }
    3.24    val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c,
    3.25 -    print_stmt: string list -> Code_Symbol.symbol * 'a -> 'c,
    3.26 +    print_stmt: string list -> Code_Symbol.T * 'a -> 'c,
    3.27      lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c }
    3.28        -> ('a, 'b) hierarchical_program -> 'c list
    3.29  end;
    3.30 @@ -48,7 +48,7 @@
    3.31  
    3.32  fun force_identifier ctxt fragments_tab force_module identifiers sym =
    3.33    case lookup_identifier identifiers sym of
    3.34 -      NONE => ((the o Symtab.lookup fragments_tab o Code_Symbol.namespace_prefix ctxt) sym, Code_Symbol.base_name sym)
    3.35 +      NONE => ((the o Symtab.lookup fragments_tab o Code_Symbol.default_prefix ctxt) sym, Code_Symbol.default_base sym)
    3.36      | SOME prefix_name => if null force_module then prefix_name
    3.37          else (force_module, snd prefix_name);
    3.38  
    3.39 @@ -57,7 +57,7 @@
    3.40      fun alias_fragments name = case module_identifiers name
    3.41       of SOME name' => Long_Name.explode name'
    3.42        | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name);
    3.43 -    val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.namespace_prefix ctxt o fst) program [];
    3.44 +    val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
    3.45    in
    3.46      fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))
    3.47        module_names Symtab.empty
    3.48 @@ -66,7 +66,7 @@
    3.49  
    3.50  (** flat program structure **)
    3.51  
    3.52 -type flat_program = ((string * Code_Thingol.stmt option) Code_Symbol.Graph.T * (string * Code_Symbol.symbol list) list) Graph.T;
    3.53 +type flat_program = ((string * Code_Thingol.stmt option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
    3.54  
    3.55  fun flat_program ctxt { module_prefix, module_name, reserved,
    3.56      identifiers, empty_nsp, namify_stmt, modify_stmt } program =
     4.1 --- a/src/Tools/Code/code_printer.ML	Sat Jan 25 23:50:49 2014 +0100
     4.2 +++ b/src/Tools/Code/code_printer.ML	Sat Jan 25 23:50:49 2014 +0100
     4.3 @@ -25,8 +25,8 @@
     4.4    val semicolon: Pretty.T list -> Pretty.T
     4.5    val doublesemicolon: Pretty.T list -> Pretty.T
     4.6    val indent: int -> Pretty.T -> Pretty.T
     4.7 -  val markup_stmt: Code_Symbol.symbol -> Pretty.T -> Pretty.T
     4.8 -  val format: Code_Symbol.symbol list -> int -> Pretty.T -> string
     4.9 +  val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T
    4.10 +  val format: Code_Symbol.T list -> int -> Pretty.T -> string
    4.11  
    4.12    val first_upper: string -> string
    4.13    val first_lower: string -> string
    4.14 @@ -36,7 +36,7 @@
    4.15    val lookup_var: var_ctxt -> string -> string
    4.16    val intro_base_names: (string -> bool) -> (string -> string)
    4.17      -> string list -> var_ctxt -> var_ctxt
    4.18 -  val intro_base_names_for: (string -> bool) -> (Code_Symbol.symbol -> string)
    4.19 +  val intro_base_names_for: (string -> bool) -> (Code_Symbol.T -> string)
    4.20      -> iterm list -> var_ctxt -> var_ctxt
    4.21    val aux_params: var_ctxt -> iterm list list -> string list
    4.22  
    4.23 @@ -94,6 +94,7 @@
    4.24  structure Code_Printer : CODE_PRINTER =
    4.25  struct
    4.26  
    4.27 +open Basic_Code_Symbol;
    4.28  open Code_Thingol;
    4.29  
    4.30  (** generic nonsense *)
    4.31 @@ -200,7 +201,7 @@
    4.32  fun intro_base_names_for no_syntax deresolve ts =
    4.33    []
    4.34    |> fold Code_Thingol.add_constsyms ts 
    4.35 -  |> intro_base_names (fn Code_Symbol.Constant const => no_syntax const | _ => true) deresolve;
    4.36 +  |> intro_base_names (fn Constant const => no_syntax const | _ => true) deresolve;
    4.37  
    4.38  
    4.39  (** pretty literals **)
    4.40 @@ -313,7 +314,7 @@
    4.41  fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
    4.42      (app as ({ sym, dom, ... }, ts)) =
    4.43    case sym of
    4.44 -    Code_Symbol.Constant const => (case const_syntax const of
    4.45 +    Constant const => (case const_syntax const of
    4.46        NONE => brackify fxy (print_app_expr some_thm vars app)
    4.47      | SOME (Plain_const_syntax (_, s)) =>
    4.48          brackify fxy (str s :: map (print_term some_thm vars BR) ts)
     5.1 --- a/src/Tools/Code/code_runtime.ML	Sat Jan 25 23:50:49 2014 +0100
     5.2 +++ b/src/Tools/Code/code_runtime.ML	Sat Jan 25 23:50:49 2014 +0100
     5.3 @@ -36,6 +36,7 @@
     5.4  structure Code_Runtime : CODE_RUNTIME =
     5.5  struct
     5.6  
     5.7 +open Basic_Code_Symbol;
     5.8  open Basic_Code_Thingol;
     5.9  
    5.10  (** evaluation **)
    5.11 @@ -53,9 +54,9 @@
    5.12  
    5.13  val _ = Theory.setup
    5.14    (Code_Target.extend_target (target, (Code_ML.target_SML, I))
    5.15 -  #> Code_Target.set_printings (Code_Symbol.Type_Constructor (@{type_name prop},
    5.16 +  #> Code_Target.set_printings (Type_Constructor (@{type_name prop},
    5.17      [(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
    5.18 -  #> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Code_Generator.holds},
    5.19 +  #> Code_Target.set_printings (Constant (@{const_name Code_Generator.holds},
    5.20      [(target, SOME (Code_Printer.plain_const_syntax s_Holds))]))
    5.21    #> Code_Target.add_reserved target this
    5.22    #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]);
    5.23 @@ -92,7 +93,7 @@
    5.24    |> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
    5.25  
    5.26  fun obtain_evaluator' thy some_target program =
    5.27 -  obtain_evaluator thy some_target program o map Code_Symbol.Constant;
    5.28 +  obtain_evaluator thy some_target program o map Constant;
    5.29  
    5.30  fun evaluation cookie thy evaluator vs_t args =
    5.31    let
    5.32 @@ -198,7 +199,7 @@
    5.33      val program = Code_Thingol.consts_program thy false consts;
    5.34      val (ml_modules, target_names) =
    5.35        Code_Target.produce_code_for thy
    5.36 -        target NONE module_name [] program (map Code_Symbol.Constant consts @ map Code_Symbol.Type_Constructor tycos);
    5.37 +        target NONE module_name [] program (map Constant consts @ map Type_Constructor tycos);
    5.38      val ml_code = space_implode "\n\n" (map snd ml_modules);
    5.39      val (consts', tycos') = chop (length consts) target_names;
    5.40      val consts_map = map2 (fn const =>
    5.41 @@ -292,7 +293,7 @@
    5.42            Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
    5.43    in
    5.44      thy
    5.45 -    |> Code_Target.set_printings (Code_Symbol.Type_Constructor (tyco, [(target, SOME (k, pr))]))
    5.46 +    |> Code_Target.set_printings (Type_Constructor (tyco, [(target, SOME (k, pr))]))
    5.47    end;
    5.48  
    5.49  fun add_eval_constr (const, const') thy =
    5.50 @@ -302,11 +303,11 @@
    5.51        (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
    5.52    in
    5.53      thy
    5.54 -    |> Code_Target.set_printings (Code_Symbol.Constant (const,
    5.55 +    |> Code_Target.set_printings (Constant (const,
    5.56        [(target, SOME (Code_Printer.simple_const_syntax (k, pr)))]))
    5.57    end;
    5.58  
    5.59 -fun add_eval_const (const, const') = Code_Target.set_printings (Code_Symbol.Constant
    5.60 +fun add_eval_const (const, const') = Code_Target.set_printings (Constant
    5.61    (const, [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')))]));
    5.62  
    5.63  fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy =
    5.64 @@ -437,7 +438,7 @@
    5.65    |> Code_Target.add_reserved target ml_name
    5.66    |> Specification.axiomatization [(b, SOME T, NoSyn)] []
    5.67    |-> (fn ([Const (const, _)], _) =>
    5.68 -    Code_Target.set_printings (Code_Symbol.Constant (const,
    5.69 +    Code_Target.set_printings (Constant (const,
    5.70        [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
    5.71    #> tap (fn thy => Code_Target.produce_code thy [const] target NONE structure_generated []));
    5.72  
     6.1 --- a/src/Tools/Code/code_scala.ML	Sat Jan 25 23:50:49 2014 +0100
     6.2 +++ b/src/Tools/Code/code_scala.ML	Sat Jan 25 23:50:49 2014 +0100
     6.3 @@ -15,6 +15,7 @@
     6.4  
     6.5  val target = "Scala";
     6.6  
     6.7 +open Basic_Code_Symbol;
     6.8  open Basic_Code_Thingol;
     6.9  open Code_Printer;
    6.10  
    6.11 @@ -27,18 +28,18 @@
    6.12  fun print_scala_stmt tyco_syntax const_syntax reserved
    6.13      args_num is_constr (deresolve, deresolve_full) =
    6.14    let
    6.15 -    val deresolve_const = deresolve o Code_Symbol.Constant;
    6.16 -    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
    6.17 -    val deresolve_class = deresolve o Code_Symbol.Type_Class;
    6.18 +    val deresolve_const = deresolve o Constant;
    6.19 +    val deresolve_tyco = deresolve o Type_Constructor;
    6.20 +    val deresolve_class = deresolve o Type_Class;
    6.21      fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
    6.22      fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
    6.23      fun print_tyco_expr tyvars fxy (sym, tys) = applify "[" "]"
    6.24            (print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys
    6.25      and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
    6.26 -         of NONE => print_tyco_expr tyvars fxy (Code_Symbol.Type_Constructor tyco, tys)
    6.27 +         of NONE => print_tyco_expr tyvars fxy (Type_Constructor tyco, tys)
    6.28            | SOME (_, print) => print (print_typ tyvars) fxy tys)
    6.29        | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
    6.30 -    fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Code_Symbol.Type_Class class, [ty]);
    6.31 +    fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Type_Class class, [ty]);
    6.32      fun print_tupled_typ tyvars ([], ty) =
    6.33            print_typ tyvars NOBR ty
    6.34        | print_tupled_typ tyvars ([ty1], ty2) =
    6.35 @@ -70,7 +71,7 @@
    6.36            end
    6.37        | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) =
    6.38            (case Code_Thingol.unfold_const_app (#primitive case_expr)
    6.39 -           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
    6.40 +           of SOME (app as ({ sym = Constant const, ... }, _)) =>
    6.41                  if is_none (const_syntax const)
    6.42                  then print_case tyvars some_thm vars fxy case_expr
    6.43                  else print_app tyvars is_pat some_thm vars fxy app
    6.44 @@ -81,7 +82,7 @@
    6.45          val k = length ts;
    6.46          val typargs' = if is_pat then [] else typargs;
    6.47          val syntax = case sym of
    6.48 -            Code_Symbol.Constant const => const_syntax const
    6.49 +            Constant const => const_syntax const
    6.50            | _ => NONE;
    6.51          val (l, print') = case syntax of
    6.52              NONE => (args_num sym, fn fxy => fn ts => gen_applify (is_constr sym) "(" ")"
    6.53 @@ -151,7 +152,7 @@
    6.54      fun print_defhead tyvars vars const vs params tys ty =
    6.55        Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
    6.56          constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
    6.57 -          NOBR (print_context tyvars vs (Code_Symbol.Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
    6.58 +          NOBR (print_context tyvars vs (Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
    6.59              str " ="];
    6.60      fun print_def const (vs, ty) [] =
    6.61            let
    6.62 @@ -204,10 +205,10 @@
    6.63                  str "match", str "{"], str "}")
    6.64                (map print_clause eqs)
    6.65            end;
    6.66 -    val print_method = str o Library.enclose "`" "`" o deresolve_full o Code_Symbol.Constant;
    6.67 -    fun print_stmt (Code_Symbol.Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
    6.68 +    val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant;
    6.69 +    fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
    6.70            print_def const (vs, ty) (filter (snd o snd) raw_eqs)
    6.71 -      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) =
    6.72 +      | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) =
    6.73            let
    6.74              val tyvars = intro_tyvars (map (rpair []) vs) reserved;
    6.75              fun print_co ((co, vs_args), tys) =
    6.76 @@ -224,7 +225,7 @@
    6.77                NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
    6.78                  :: map print_co cos)
    6.79            end
    6.80 -      | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
    6.81 +      | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
    6.82            let
    6.83              val tyvars = intro_tyvars [(v, [class])] reserved;
    6.84              fun add_typarg s = Pretty.block
    6.85 @@ -349,12 +350,12 @@
    6.86        scala_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
    6.87  
    6.88      (* print statements *)
    6.89 -    fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Code_Symbol.Type_Constructor tyco)
    6.90 +    fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Type_Constructor tyco)
    6.91       of Code_Thingol.Datatype (_, constrs) =>
    6.92            the (AList.lookup (op = o apsnd fst) constrs constr);
    6.93 -    fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Code_Symbol.Type_Class class)
    6.94 +    fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Type_Class class)
    6.95       of Code_Thingol.Class (_, (_, classparams)) => classparams;
    6.96 -    fun args_num (sym as Code_Symbol.Constant const) = case Code_Symbol.Graph.get_node program sym
    6.97 +    fun args_num (sym as Constant const) = case Code_Symbol.Graph.get_node program sym
    6.98       of Code_Thingol.Fun (((_, ty), []), _) =>
    6.99            (length o fst o Code_Thingol.unfold_fun) ty
   6.100        | Code_Thingol.Fun ((_, ((ts, _), _) :: _), _) => length ts
   6.101 @@ -422,7 +423,7 @@
   6.102          make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
   6.103          make_command = fn _ =>
   6.104            "env JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' \"$SCALA_HOME/bin/scalac\" ROOT.scala" } })
   6.105 -  #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
   6.106 +  #> Code_Target.set_printings (Type_Constructor ("fun",
   6.107      [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   6.108        brackify_infix (1, R) fxy (
   6.109          print_typ BR ty1 (*product type vs. tupled arguments!*),
     7.1 --- a/src/Tools/Code/code_symbol.ML	Sat Jan 25 23:50:49 2014 +0100
     7.2 +++ b/src/Tools/Code/code_symbol.ML	Sat Jan 25 23:50:49 2014 +0100
     7.3 @@ -5,20 +5,25 @@
     7.4  class relations, class instances, modules.
     7.5  *)
     7.6  
     7.7 -signature CODE_SYMBOL =
     7.8 +signature BASIC_CODE_SYMBOL =
     7.9  sig
    7.10    datatype ('a, 'b, 'c, 'd, 'e, 'f) attr =
    7.11      Constant of 'a | Type_Constructor of 'b | Type_Class of 'c |
    7.12      Class_Relation of 'd  | Class_Instance of 'e | Module of 'f
    7.13 -  type symbol = (string, string, class, class * class, string * class, string) attr
    7.14 -  structure Table: TABLE;
    7.15 -  structure Graph: GRAPH;
    7.16 -  val namespace_prefix: Proof.context -> symbol -> string
    7.17 -  val base_name: symbol -> string
    7.18 -  val quote: Proof.context -> symbol -> string
    7.19 -  val marker: symbol -> string
    7.20 -  val value: symbol
    7.21 -  val is_value: symbol -> bool
    7.22 +end
    7.23 +
    7.24 +signature CODE_SYMBOL =
    7.25 +sig
    7.26 +  include BASIC_CODE_SYMBOL
    7.27 +  type T = (string, string, class, class * class, string * class, string) attr
    7.28 +  structure Table: TABLE
    7.29 +  structure Graph: GRAPH
    7.30 +  val default_base: T -> string
    7.31 +  val default_prefix: Proof.context -> T -> string
    7.32 +  val quote: Proof.context -> T -> string
    7.33 +  val marker: T -> string
    7.34 +  val value: T
    7.35 +  val is_value: T -> bool
    7.36    val map_attr: ('a -> 'g) -> ('b -> 'h) -> ('c -> 'i) -> ('d -> 'j) -> ('e -> 'k) -> ('f -> 'l)
    7.37      -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr
    7.38    val maps_attr: ('a -> 'g list) -> ('b -> 'h list)
    7.39 @@ -40,8 +45,8 @@
    7.40    val lookup_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class * class -> 'd option
    7.41    val lookup_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string * class -> 'e option
    7.42    val lookup_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'f option
    7.43 -  val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> symbol -> 'a option
    7.44 -  val symbols_of: ('a, 'b, 'c, 'd, 'e, 'f) data -> symbol list
    7.45 +  val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> T -> 'a option
    7.46 +  val symbols_of: ('a, 'b, 'c, 'd, 'e, 'f) data -> T list
    7.47    val dest_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'f) list
    7.48  end;
    7.49  
    7.50 @@ -53,7 +58,7 @@
    7.51  datatype ('a, 'b, 'c, 'd, 'e, 'f) attr =
    7.52    Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | Class_Relation of 'd  | Class_Instance of 'e | Module of 'f;
    7.53  
    7.54 -type symbol = (string, string, class, string * class, class * class, string) attr;
    7.55 +type T = (string, string, class, string * class, class * class, string) attr;
    7.56  
    7.57  fun symbol_ord (Constant c1, Constant c2) = fast_string_ord (c1, c2)
    7.58    | symbol_ord (Constant _, _) = GREATER
    7.59 @@ -74,8 +79,24 @@
    7.60    | symbol_ord (_, Class_Instance _) = LESS
    7.61    | symbol_ord (Module name1, Module name2) = fast_string_ord (name1, name2);
    7.62  
    7.63 -structure Table = Table(type key = symbol val ord = symbol_ord);
    7.64 -structure Graph = Graph(type key = symbol val ord = symbol_ord);
    7.65 +structure Table = Table(type key = T val ord = symbol_ord);
    7.66 +structure Graph = Graph(type key = T val ord = symbol_ord);
    7.67 +
    7.68 +local
    7.69 +  val base = Name.desymbolize false o Long_Name.base_name;
    7.70 +  fun base_rel (x, y) = base y ^ "_" ^ base x;
    7.71 +in
    7.72 +
    7.73 +fun default_base (Constant "") = "value"
    7.74 +  | default_base (Constant "==>") = "follows"
    7.75 +  | default_base (Constant "==") = "meta_eq"
    7.76 +  | default_base (Constant c) = base c
    7.77 +  | default_base (Type_Constructor tyco) = base tyco
    7.78 +  | default_base (Type_Class class) = base class
    7.79 +  | default_base (Class_Relation classrel) = base_rel classrel
    7.80 +  | default_base (Class_Instance inst) = base_rel inst;
    7.81 +
    7.82 +end;
    7.83  
    7.84  local
    7.85    fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
    7.86 @@ -94,29 +115,16 @@
    7.87      | prefix thy (Type_Class class) = thyname_of_class thy class
    7.88      | prefix thy (Class_Relation (class, _)) = thyname_of_class thy class
    7.89      | prefix thy (Class_Instance inst) = thyname_of_instance thy inst;
    7.90 -  val base = Name.desymbolize false o Long_Name.base_name;
    7.91 -  fun base_rel (x, y) = base y ^ "_" ^ base x;
    7.92  in
    7.93  
    7.94 -fun base_name (Constant "") = "value"
    7.95 -  | base_name (Constant "==>") = "follows"
    7.96 -  | base_name (Constant "==") = "meta_eq"
    7.97 -  | base_name (Constant c) = base c
    7.98 -  | base_name (Type_Constructor tyco) = base tyco
    7.99 -  | base_name (Type_Class class) = base class
   7.100 -  | base_name (Class_Relation classrel) = base_rel classrel
   7.101 -  | base_name (Class_Instance inst) = base_rel inst;
   7.102 +fun default_prefix ctxt = prefix (Proof_Context.theory_of ctxt);
   7.103  
   7.104 -fun namespace_prefix ctxt = prefix (Proof_Context.theory_of ctxt);
   7.105 -
   7.106 -fun default_name ctxt sym = (namespace_prefix ctxt sym, base_name sym);
   7.107 +end;
   7.108  
   7.109  val value = Constant "";
   7.110  fun is_value (Constant "") = true
   7.111    | is_value _ = false;
   7.112  
   7.113 -end;
   7.114 -
   7.115  fun quote ctxt (Constant c) = Library.quote (Code.string_of_const (Proof_Context.theory_of ctxt) c)
   7.116    | quote ctxt (Type_Constructor tyco) = "type " ^ Library.quote (Proof_Context.extern_type ctxt tyco)
   7.117    | quote ctxt (Type_Class class) = "class " ^ Library.quote (Proof_Context.extern_class ctxt class)
   7.118 @@ -216,3 +224,6 @@
   7.119  fun dest_module_data x = (Symtab.dest o #module o dest_data) x;
   7.120  
   7.121  end;
   7.122 +
   7.123 +
   7.124 +structure Basic_Code_Symbol: BASIC_CODE_SYMBOL = Code_Symbol;
     8.1 --- a/src/Tools/Code/code_target.ML	Sat Jan 25 23:50:49 2014 +0100
     8.2 +++ b/src/Tools/Code/code_target.ML	Sat Jan 25 23:50:49 2014 +0100
     8.3 @@ -11,26 +11,26 @@
     8.4    val read_const_exprs: theory -> string list -> string list
     8.5  
     8.6    val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
     8.7 -    -> Code_Thingol.program -> Code_Symbol.symbol list -> unit
     8.8 +    -> Code_Thingol.program -> Code_Symbol.T list -> unit
     8.9    val produce_code_for: theory -> string -> int option -> string -> Token.T list
    8.10 -    -> Code_Thingol.program -> Code_Symbol.symbol list -> (string * string) list * string option list
    8.11 +    -> Code_Thingol.program -> Code_Symbol.T list -> (string * string) list * string option list
    8.12    val present_code_for: theory -> string -> int option -> string -> Token.T list
    8.13 -    -> Code_Thingol.program -> Code_Symbol.symbol list * Code_Symbol.symbol list -> string
    8.14 +    -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string
    8.15    val check_code_for: theory -> string -> bool -> Token.T list
    8.16 -    -> Code_Thingol.program -> Code_Symbol.symbol list -> unit
    8.17 +    -> Code_Thingol.program -> Code_Symbol.T list -> unit
    8.18  
    8.19    val export_code: theory -> string list
    8.20      -> (((string * string) * Path.T option) * Token.T list) list -> unit
    8.21    val produce_code: theory -> string list
    8.22      -> string -> int option -> string -> Token.T list -> (string * string) list * string option list
    8.23 -  val present_code: theory -> string list -> Code_Symbol.symbol list
    8.24 +  val present_code: theory -> string list -> Code_Symbol.T list
    8.25      -> string -> int option -> string -> Token.T list -> string
    8.26    val check_code: theory -> string list
    8.27      -> ((string * bool) * Token.T list) list -> unit
    8.28  
    8.29    val generatedN: string
    8.30    val evaluator: theory -> string -> Code_Thingol.program
    8.31 -    -> Code_Symbol.symbol list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
    8.32 +    -> Code_Symbol.T list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
    8.33      -> (string * string) list * string
    8.34  
    8.35    type serializer
    8.36 @@ -46,7 +46,7 @@
    8.37    type serialization
    8.38    val parse_args: 'a parser -> Token.T list -> 'a
    8.39    val serialization: (int -> Path.T option -> 'a -> unit)
    8.40 -    -> (Code_Symbol.symbol list -> int -> 'a -> (string * string) list * (Code_Symbol.symbol -> string option))
    8.41 +    -> (Code_Symbol.T list -> int -> 'a -> (string * string) list * (Code_Symbol.T -> string option))
    8.42      -> 'a -> serialization
    8.43    val set_default_code_width: int -> theory -> theory
    8.44  
    8.45 @@ -73,6 +73,7 @@
    8.46  structure Code_Target : CODE_TARGET =
    8.47  struct
    8.48  
    8.49 +open Basic_Code_Symbol;
    8.50  open Basic_Code_Thingol;
    8.51  
    8.52  type literals = Code_Printer.literals;
    8.53 @@ -154,8 +155,8 @@
    8.54  
    8.55  (* serialization: abstract nonsense to cover different destinies for generated code *)
    8.56  
    8.57 -datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.symbol list;
    8.58 -type serialization = int -> destination -> ((string * string) list * (Code_Symbol.symbol -> string option)) option;
    8.59 +datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.T list;
    8.60 +type serialization = int -> destination -> ((string * string) list * (Code_Symbol.T -> string option)) option;
    8.61  
    8.62  fun serialization output _ content width (Export some_path) =
    8.63        (output width some_path content; NONE)
    8.64 @@ -345,7 +346,7 @@
    8.65      val syms_hidden = Code_Symbol.symbols_of printings;
    8.66      val (syms_all, program) = project_program thy syms_hidden syms proto_program;
    8.67      fun select_include (name, (content, cs)) =
    8.68 -      if null cs orelse exists (fn c => member (op =) syms_all (Code_Symbol.Constant c)) cs
    8.69 +      if null cs orelse exists (fn c => member (op =) syms_all (Constant c)) cs
    8.70        then SOME (name, content) else NONE;
    8.71      val includes = map_filter select_include (Code_Symbol.dest_module_data printings);
    8.72    in
    8.73 @@ -471,7 +472,7 @@
    8.74    let
    8.75      val program = Code_Thingol.consts_program thy false cs;
    8.76      val _ = map (fn (((target, module_name), some_path), args) =>
    8.77 -      export_code_for thy some_path target NONE module_name args program (map Code_Symbol.Constant cs)) seris;
    8.78 +      export_code_for thy some_path target NONE module_name args program (map Constant cs)) seris;
    8.79    in () end;
    8.80  
    8.81  fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs)
    8.82 @@ -480,18 +481,18 @@
    8.83  fun produce_code thy cs target some_width some_module_name args =
    8.84    let
    8.85      val program = Code_Thingol.consts_program thy false cs;
    8.86 -  in produce_code_for thy target some_width some_module_name args program (map Code_Symbol.Constant cs) end;
    8.87 +  in produce_code_for thy target some_width some_module_name args program (map Constant cs) end;
    8.88  
    8.89  fun present_code thy cs syms target some_width some_module_name args =
    8.90    let
    8.91      val program = Code_Thingol.consts_program thy false cs;
    8.92 -  in present_code_for thy target some_width some_module_name args program (map Code_Symbol.Constant cs, syms) end;
    8.93 +  in present_code_for thy target some_width some_module_name args program (map Constant cs, syms) end;
    8.94  
    8.95  fun check_code thy cs seris =
    8.96    let
    8.97      val program = Code_Thingol.consts_program thy false cs;
    8.98      val _ = map (fn ((target, strict), args) =>
    8.99 -      check_code_for thy target strict args program (map Code_Symbol.Constant cs)) seris;
   8.100 +      check_code_for thy target strict args program (map Constant cs)) seris;
   8.101    in () end;
   8.102  
   8.103  fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;
   8.104 @@ -506,17 +507,17 @@
   8.105    >> (fn xs => fn thy => map (mark_symbol o internalize thy) xs);
   8.106  
   8.107  val parse_consts = parse_names "consts" Args.term
   8.108 -  Code.check_const Code_Symbol.Constant;
   8.109 +  Code.check_const Constant;
   8.110  
   8.111  val parse_types = parse_names "types" (Scan.lift Args.name)
   8.112 -  Sign.intern_type Code_Symbol.Type_Constructor;
   8.113 +  Sign.intern_type Type_Constructor;
   8.114  
   8.115  val parse_classes = parse_names "classes" (Scan.lift Args.name)
   8.116 -  Sign.intern_class Code_Symbol.Type_Class;
   8.117 +  Sign.intern_class Type_Class;
   8.118  
   8.119  val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
   8.120    (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class))
   8.121 -    Code_Symbol.Class_Instance;
   8.122 +    Class_Instance;
   8.123  
   8.124  in
   8.125  
   8.126 @@ -630,19 +631,19 @@
   8.127    in set_printing (target, Symbol (x, Option.map (prep_syn thy target x) some_raw_syn)) thy end;
   8.128  
   8.129  fun gen_add_const_syntax prep_const =
   8.130 -  gen_add_syntax Code_Symbol.Constant prep_const check_const_syntax;
   8.131 +  gen_add_syntax Constant prep_const check_const_syntax;
   8.132  
   8.133  fun gen_add_tyco_syntax prep_tyco =
   8.134 -  gen_add_syntax Code_Symbol.Type_Constructor prep_tyco check_tyco_syntax;
   8.135 +  gen_add_syntax Type_Constructor prep_tyco check_tyco_syntax;
   8.136  
   8.137  fun gen_add_class_syntax prep_class =
   8.138 -  gen_add_syntax Code_Symbol.Type_Class prep_class ((K o K o K) I);
   8.139 +  gen_add_syntax Type_Class prep_class ((K o K o K) I);
   8.140  
   8.141  fun gen_add_instance_syntax prep_inst =
   8.142 -  gen_add_syntax Code_Symbol.Class_Instance prep_inst ((K o K o K) I);
   8.143 +  gen_add_syntax Class_Instance prep_inst ((K o K o K) I);
   8.144  
   8.145  fun gen_add_include prep_const target (name, some_content) thy =
   8.146 -  gen_add_syntax Code_Symbol.Module (K I)
   8.147 +  gen_add_syntax Module (K I)
   8.148      (fn thy => fn _ => fn _ => fn (raw_content, raw_cs) => (Code_Printer.str raw_content, map (prep_const thy) raw_cs))
   8.149      target name some_content thy;
   8.150  
   8.151 @@ -693,15 +694,15 @@
   8.152  
   8.153  fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
   8.154    parse_single_symbol_pragma @{keyword "constant"} Parse.term parse_const
   8.155 -    >> Code_Symbol.Constant
   8.156 +    >> Constant
   8.157    || parse_single_symbol_pragma @{keyword "type_constructor"} Parse.type_const parse_tyco
   8.158 -    >> Code_Symbol.Type_Constructor
   8.159 +    >> Type_Constructor
   8.160    || parse_single_symbol_pragma @{keyword "type_class"} Parse.class parse_class
   8.161 -    >> Code_Symbol.Type_Class
   8.162 +    >> Type_Class
   8.163    || parse_single_symbol_pragma @{keyword "class_relation"} parse_classrel_ident parse_classrel
   8.164 -    >> Code_Symbol.Class_Relation
   8.165 +    >> Class_Relation
   8.166    || parse_single_symbol_pragma @{keyword "class_instance"} parse_inst_ident parse_inst
   8.167 -    >> Code_Symbol.Class_Instance
   8.168 +    >> Class_Instance
   8.169    || parse_single_symbol_pragma @{keyword "code_module"} Parse.name parse_module
   8.170      >> Code_Symbol.Module;
   8.171  
     9.1 --- a/src/Tools/Code/code_thingol.ML	Sat Jan 25 23:50:49 2014 +0100
     9.2 +++ b/src/Tools/Code/code_thingol.ML	Sat Jan 25 23:50:49 2014 +0100
     9.3 @@ -23,7 +23,7 @@
     9.4    datatype itype =
     9.5        `%% of string * itype list
     9.6      | ITyVar of vname;
     9.7 -  type const = { sym: Code_Symbol.symbol, typargs: itype list, dicts: dict list list,
     9.8 +  type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
     9.9      dom: itype list, range: itype, annotate: bool };
    9.10    datatype iterm =
    9.11        IConst of const
    9.12 @@ -55,7 +55,7 @@
    9.13    val is_IAbs: iterm -> bool
    9.14    val eta_expand: int -> const * iterm list -> iterm
    9.15    val contains_dict_var: iterm -> bool
    9.16 -  val add_constsyms: iterm -> Code_Symbol.symbol list -> Code_Symbol.symbol list
    9.17 +  val add_constsyms: iterm -> Code_Symbol.T list -> Code_Symbol.T list
    9.18    val add_tyconames: iterm -> string list -> string list
    9.19    val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
    9.20  
    9.21 @@ -77,34 +77,36 @@
    9.22    val implemented_deps: program -> string list
    9.23    val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
    9.24    val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
    9.25 -  val is_constr: program -> Code_Symbol.symbol -> bool
    9.26 +  val is_constr: program -> Code_Symbol.T -> bool
    9.27    val is_case: stmt -> bool
    9.28    val group_stmts: theory -> program
    9.29 -    -> ((Code_Symbol.symbol * stmt) list * (Code_Symbol.symbol * stmt) list
    9.30 -      * ((Code_Symbol.symbol * stmt) list * (Code_Symbol.symbol * stmt) list)) list
    9.31 +    -> ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list
    9.32 +      * ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list
    9.33  
    9.34    val read_const_exprs: theory -> string list -> string list * string list
    9.35    val consts_program: theory -> bool -> string list -> program
    9.36    val dynamic_conv: theory -> (program
    9.37 -    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> conv)
    9.38 +    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
    9.39      -> conv
    9.40    val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (program
    9.41 -    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> 'a)
    9.42 +    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
    9.43      -> term -> 'a
    9.44    val static_conv: theory -> string list -> (program -> string list
    9.45 -    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> conv)
    9.46 +    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
    9.47      -> conv
    9.48    val static_conv_simple: theory -> string list
    9.49      -> (program -> (string * sort) list -> term -> conv) -> conv
    9.50    val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
    9.51      (program -> string list
    9.52 -      -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> 'a)
    9.53 +      -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
    9.54      -> term -> 'a
    9.55  end;
    9.56  
    9.57  structure Code_Thingol: CODE_THINGOL =
    9.58  struct
    9.59  
    9.60 +open Basic_Code_Symbol;
    9.61 +
    9.62  (** auxiliary **)
    9.63  
    9.64  fun unfoldl dest x =
    9.65 @@ -147,7 +149,7 @@
    9.66      val ty3 = Library.foldr (op `->) (tys2, ty1);
    9.67    in (tys3, ty3) end;
    9.68  
    9.69 -type const = { sym: Code_Symbol.symbol, typargs: itype list, dicts: dict list list,
    9.70 +type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
    9.71    dom: itype list, range: itype, annotate: bool };
    9.72  
    9.73  datatype iterm =
    9.74 @@ -286,12 +288,12 @@
    9.75  type program = stmt Code_Symbol.Graph.T;
    9.76  
    9.77  fun unimplemented program =
    9.78 -  Code_Symbol.Graph.fold (fn (Code_Symbol.Constant c, (NoStmt, _)) => cons c | _ => I) program [];
    9.79 +  Code_Symbol.Graph.fold (fn (Constant c, (NoStmt, _)) => cons c | _ => I) program [];
    9.80  
    9.81  fun implemented_deps program =
    9.82    Code_Symbol.Graph.keys program
    9.83 -  |> subtract (op =) (Code_Symbol.Graph.all_preds program (map Code_Symbol.Constant (unimplemented program)))
    9.84 -  |> map_filter (fn Code_Symbol.Constant c => SOME c | _ => NONE);
    9.85 +  |> subtract (op =) (Code_Symbol.Graph.all_preds program (map Constant (unimplemented program)))
    9.86 +  |> map_filter (fn Constant c => SOME c | _ => NONE);
    9.87  
    9.88  fun map_terms_bottom_up f (t as IConst _) = f t
    9.89    | map_terms_bottom_up f (t as IVar _) = f t
    9.90 @@ -466,7 +468,7 @@
    9.91          ##>> pair (map (unprefix "'" o fst) vs)
    9.92          ##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
    9.93        #>> Datatype;
    9.94 -  in ensure_stmt Code_Symbol.Type_Constructor stmt_datatype tyco end
    9.95 +  in ensure_stmt Type_Constructor stmt_datatype tyco end
    9.96  and ensure_const thy algbr eqngr permissive c =
    9.97    let
    9.98      fun stmt_datatypecons tyco =
    9.99 @@ -494,7 +496,7 @@
   9.100        | NONE => (case Axclass.class_of_param thy c
   9.101           of SOME class => stmt_classparam class
   9.102            | NONE => stmt_fun (Code_Preproc.cert eqngr c))
   9.103 -  in ensure_stmt Code_Symbol.Constant stmt_const c end
   9.104 +  in ensure_stmt Constant stmt_const c end
   9.105  and ensure_class thy (algbr as (_, algebra)) eqngr permissive class =
   9.106    let
   9.107      val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
   9.108 @@ -505,14 +507,14 @@
   9.109        ##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
   9.110          ##>> translate_typ thy algbr eqngr permissive ty) cs
   9.111        #>> (fn info => Class (unprefix "'" Name.aT, info))
   9.112 -  in ensure_stmt Code_Symbol.Type_Class stmt_class class end
   9.113 +  in ensure_stmt Type_Class stmt_class class end
   9.114  and ensure_classrel thy algbr eqngr permissive (sub_class, super_class) =
   9.115    let
   9.116      val stmt_classrel =
   9.117        ensure_class thy algbr eqngr permissive sub_class
   9.118        ##>> ensure_class thy algbr eqngr permissive super_class
   9.119        #>> Classrel;
   9.120 -  in ensure_stmt Code_Symbol.Class_Relation stmt_classrel (sub_class, super_class) end
   9.121 +  in ensure_stmt Class_Relation stmt_classrel (sub_class, super_class) end
   9.122  and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (tyco, class) =
   9.123    let
   9.124      val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
   9.125 @@ -552,7 +554,7 @@
   9.126        #>> (fn (((((class, tyco), vs), superinsts), inst_params), superinst_params) =>
   9.127            Classinst { class = class, tyco = tyco, vs = vs,
   9.128              superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params });
   9.129 -  in ensure_stmt Code_Symbol.Class_Instance stmt_inst (tyco, class) end
   9.130 +  in ensure_stmt Class_Instance stmt_inst (tyco, class) end
   9.131  and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
   9.132        pair (ITyVar (unprefix "'" v))
   9.133    | translate_typ thy algbr eqngr permissive (Type (tyco, tys)) =
   9.134 @@ -604,7 +606,7 @@
   9.135      ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (typargs ~~ sorts)
   9.136      ##>> fold_map (translate_typ thy algbr eqngr permissive) (range :: dom)
   9.137      #>> (fn (((c, typargs), dss), range :: dom) =>
   9.138 -      IConst { sym = Code_Symbol.Constant c, typargs = typargs, dicts = dss,
   9.139 +      IConst { sym = Constant c, typargs = typargs, dicts = dss,
   9.140          dom = dom, range = range, annotate = annotate })
   9.141    end
   9.142  and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
   9.143 @@ -629,7 +631,7 @@
   9.144        let
   9.145          fun collapse_clause vs_map ts body =
   9.146            case body
   9.147 -           of IConst { sym = Code_Symbol.Constant c, ... } => if member (op =) undefineds c
   9.148 +           of IConst { sym = Constant c, ... } => if member (op =) undefineds c
   9.149                  then []
   9.150                  else [(ts, body)]
   9.151              | ICase { term = IVar (SOME v), clauses = clauses, ... } =>
   9.152 @@ -747,7 +749,7 @@
   9.153        if permissive then program
   9.154        else Code_Symbol.Graph.restrict
   9.155          (member (op =) (Code_Symbol.Graph.all_succs program
   9.156 -          (map Code_Symbol.Constant consts))) program;
   9.157 +          (map Constant consts))) program;
   9.158      fun generate_consts thy algebra eqngr =
   9.159        fold_map (ensure_const thy algebra eqngr permissive);
   9.160    in
   9.161 @@ -766,7 +768,7 @@
   9.162      val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
   9.163        o dest_TFree))) t [];
   9.164      val t' = annotate thy algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
   9.165 -    val dummy_constant = Code_Symbol.Constant @{const_name dummy_pattern};
   9.166 +    val dummy_constant = Constant @{const_name dummy_pattern};
   9.167      val stmt_value =
   9.168        fold_map (translate_tyvar_sort thy algbr eqngr false) vs
   9.169        ##>> translate_typ thy algbr eqngr false ty
   9.170 @@ -783,7 +785,7 @@
   9.171          val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2;
   9.172        in ((program3, ((vs_ty, t), deps)), (dep, program2)) end;
   9.173    in
   9.174 -    ensure_stmt Code_Symbol.Constant stmt_value @{const_name dummy_pattern}
   9.175 +    ensure_stmt Constant stmt_value @{const_name dummy_pattern}
   9.176      #> snd
   9.177      #> term_value
   9.178    end;
    10.1 --- a/src/Tools/nbe.ML	Sat Jan 25 23:50:49 2014 +0100
    10.2 +++ b/src/Tools/nbe.ML	Sat Jan 25 23:50:49 2014 +0100
    10.3 @@ -249,11 +249,9 @@
    10.4  
    10.5  val univs_cookie = (Univs.get, put_result, name_put);
    10.6  
    10.7 -val sloppy_name = Code_Symbol.base_name;
    10.8 -
    10.9  fun nbe_fun idx_of 0 (Code_Symbol.Constant "") = "nbe_value"
   10.10    | nbe_fun idx_of i sym = "c_" ^ string_of_int (idx_of sym)
   10.11 -      ^ "_" ^ sloppy_name sym ^ "_" ^ string_of_int i;
   10.12 +      ^ "_" ^ Code_Symbol.default_base sym ^ "_" ^ string_of_int i;
   10.13  fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n;
   10.14  fun nbe_bound v = "v_" ^ v;
   10.15  fun nbe_bound_optional NONE = "_"
   10.16 @@ -266,7 +264,7 @@
   10.17  fun nbe_apps_local idx_of i c ts = nbe_fun idx_of i c `$` ml_list (rev ts);
   10.18  fun nbe_apps_constr idx_of c ts =
   10.19    let
   10.20 -    val c' = if !trace then string_of_int (idx_of c) ^ " (*" ^ sloppy_name c ^ "*)"
   10.21 +    val c' = if !trace then string_of_int (idx_of c) ^ " (*" ^ Code_Symbol.default_base c ^ "*)"
   10.22        else string_of_int (idx_of c);
   10.23    in name_const `$` ("(" ^ c' ^ ", " ^ ml_list (rev ts) ^ ")") end;
   10.24  
   10.25 @@ -277,6 +275,7 @@
   10.26  
   10.27  end;
   10.28  
   10.29 +open Basic_Code_Symbol;
   10.30  open Basic_Code_Thingol;
   10.31  
   10.32  
   10.33 @@ -304,11 +303,11 @@
   10.34              else nbe_apps_constr idx_of sym ts'
   10.35        end
   10.36      and assemble_classrels classrels =
   10.37 -      fold_rev (fn classrel => assemble_constapp (Code_Symbol.Class_Relation classrel) [] o single) classrels
   10.38 +      fold_rev (fn classrel => assemble_constapp (Class_Relation classrel) [] o single) classrels
   10.39      and assemble_dict (Dict (classrels, x)) =
   10.40            assemble_classrels classrels (assemble_plain_dict x)
   10.41      and assemble_plain_dict (Dict_Const (inst, dss)) =
   10.42 -          assemble_constapp (Code_Symbol.Class_Instance inst) dss []
   10.43 +          assemble_constapp (Class_Instance inst) dss []
   10.44        | assemble_plain_dict (Dict_Var (v, (n, _))) =
   10.45            nbe_dict v n
   10.46  
   10.47 @@ -429,7 +428,7 @@
   10.48        []
   10.49    | eqns_of_stmt (sym_class, Code_Thingol.Class (v, (classrels, classparams))) =
   10.50        let
   10.51 -        val syms = map Code_Symbol.Class_Relation classrels @ map (Code_Symbol.Constant o fst) classparams;
   10.52 +        val syms = map Class_Relation classrels @ map (Constant o fst) classparams;
   10.53          val params = Name.invent Name.context "d" (length syms);
   10.54          fun mk (k, sym) =
   10.55            (sym, ([(v, [])],
   10.56 @@ -441,8 +440,8 @@
   10.57    | eqns_of_stmt (_, Code_Thingol.Classparam _) =
   10.58        []
   10.59    | eqns_of_stmt (sym_inst, Code_Thingol.Classinst { class, tyco, vs, superinsts, inst_params, ... }) =
   10.60 -      [(sym_inst, (vs, [([], dummy_const (Code_Symbol.Type_Class class) [] `$$
   10.61 -        map (fn (class, dss) => dummy_const (Code_Symbol.Class_Instance (tyco, class)) dss) superinsts
   10.62 +      [(sym_inst, (vs, [([], dummy_const (Type_Class class) [] `$$
   10.63 +        map (fn (class, dss) => dummy_const (Class_Instance (tyco, class)) dss) superinsts
   10.64          @ map (IConst o fst o snd o fst) inst_params)]))];
   10.65  
   10.66  
   10.67 @@ -513,12 +512,12 @@
   10.68        | take_until f (x :: xs) = if f x then [] else x :: take_until f xs;
   10.69      fun is_dict (Const (idx, _)) =
   10.70            (case Inttab.lookup idx_tab idx of
   10.71 -            SOME (Code_Symbol.Constant _) => false
   10.72 +            SOME (Constant _) => false
   10.73            | _ => true)
   10.74        | is_dict (DFree _) = true
   10.75        | is_dict _ = false;
   10.76      fun const_of_idx idx =
   10.77 -      case Inttab.lookup idx_tab idx of SOME (Code_Symbol.Constant const) => const;
   10.78 +      case Inttab.lookup idx_tab idx of SOME (Constant const) => const;
   10.79      fun of_apps bounds (t, ts) =
   10.80        fold_map (of_univ bounds) ts
   10.81        #>> (fn ts' => list_comb (t, rev ts'))
   10.82 @@ -568,7 +567,7 @@
   10.83  
   10.84  structure Nbe_Functions = Code_Data
   10.85  (
   10.86 -  type T = (Univ option * int) Code_Symbol.Graph.T * (int * Code_Symbol.symbol Inttab.table);
   10.87 +  type T = (Univ option * int) Code_Symbol.Graph.T * (int * Code_Symbol.T Inttab.table);
   10.88    val empty = (Code_Symbol.Graph.empty, (0, Inttab.empty));
   10.89  );
   10.90