# HG changeset patch
# User haftmann
# Date 1390690249 -3600
# Node ID 0940309ed8f1a71647f428e10d4afde4734df725
# Parent  626d8f08d479a0d669849e8354535ce1ede28621
less clumsy namespace

diff -r 626d8f08d479 -r 0940309ed8f1 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_haskell.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -25,6 +25,7 @@
 val language_params =
   space_implode " " (map (prefix "-X") language_extensions);
 
+open Basic_Code_Symbol;
 open Basic_Code_Thingol;
 open Code_Printer;
 
@@ -37,9 +38,9 @@
 fun print_haskell_stmt class_syntax tyco_syntax const_syntax
     reserved deresolve deriving_show =
   let
-    val deresolve_const = deresolve o Code_Symbol.Constant;
-    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
-    val deresolve_class = deresolve o Code_Symbol.Type_Class;
+    val deresolve_const = deresolve o Constant;
+    val deresolve_tyco = deresolve o Type_Constructor;
+    val deresolve_class = deresolve o Type_Class;
     fun class_name class = case class_syntax class
      of NONE => deresolve_class class
       | SOME class => class;
@@ -84,7 +85,7 @@
           in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
       | print_term tyvars some_thm vars fxy (ICase case_expr) =
           (case Code_Thingol.unfold_const_app (#primitive case_expr)
-           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
+           of SOME (app as ({ sym = Constant const, ... }, _)) =>
                 if is_none (const_syntax const)
                 then print_case tyvars some_thm vars fxy case_expr
                 else print_app tyvars some_thm vars fxy app
@@ -126,7 +127,7 @@
             (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
             (map print_select clauses)
           end;
-    fun print_stmt (Code_Symbol.Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
+    fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
             fun print_err n =
@@ -163,7 +164,7 @@
                 | eqs => map print_eqn eqs)
             )
           end
-      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) =
+      | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) =
           let
             val tyvars = intro_vars vs reserved;
           in
@@ -172,7 +173,7 @@
               print_typdecl tyvars (deresolve_tyco tyco, vs)
             ]
           end
-      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) =
+      | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) =
           let
             val tyvars = intro_vars vs reserved;
           in
@@ -185,7 +186,7 @@
               :: (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
             )
           end
-      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
+      | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
           let
             val tyvars = intro_vars vs reserved;
             fun print_co ((co, _), tys) =
@@ -203,7 +204,7 @@
               @ (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
             )
           end
-      | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
+      | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
           let
             val tyvars = intro_vars [v] reserved;
             fun print_classparam (classparam, ty) =
@@ -239,14 +240,14 @@
                     ]
                 | SOME k =>
                     let
-                      val { sym = Code_Symbol.Constant c, dom, range, ... } = const;
+                      val { sym = Constant c, dom, range, ... } = const;
                       val (vs, rhs) = (apfst o map) fst
                         (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
                       val s = if (is_some o const_syntax) c
                         then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
                       val vars = reserved
                         |> intro_vars (map_filter I (s :: vs));
-                      val lhs = IConst { sym = Code_Symbol.Constant classparam, typargs = [],
+                      val lhs = IConst { sym = Constant classparam, typargs = [],
                         dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
                         (*dictionaries are not relevant at this late stage,
                           and these consts never need type annotations for disambiguation *)
@@ -340,7 +341,7 @@
       let
         fun deriv _ "fun" = false
           | deriv tycos tyco = member (op =) tycos tyco
-              orelse case try (Code_Symbol.Graph.get_node program) (Code_Symbol.Type_Constructor tyco)
+              orelse case try (Code_Symbol.Graph.get_node program) (Type_Constructor tyco)
                 of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
                     (maps snd cs)
                  | NONE => true
@@ -432,7 +433,7 @@
      of SOME ((pat, ty), t') =>
           SOME ((SOME ((pat, ty), true), t1), t')
       | NONE => NONE;
-    fun dest_monad (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
+    fun dest_monad (IConst { sym = Constant c, ... } `$ t1 `$ t2) =
           if c = c_bind then dest_bind t1 t2
           else NONE
       | dest_monad t = case Code_Thingol.split_let t
@@ -467,7 +468,7 @@
   in
     if target = target' then
       thy
-      |> Code_Target.set_printings (Code_Symbol.Constant (c_bind, [(target,
+      |> Code_Target.set_printings (Constant (c_bind, [(target,
         SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))]))
     else error "Only Haskell target allows for monad syntax"
   end;
@@ -487,7 +488,7 @@
         make_command = fn module_name =>
           "\"$ISABELLE_GHC\" " ^ language_params  ^ " -odir build -hidir build -stubdir build -e \"\" " ^
             module_name ^ ".hs" } })
-  #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
+  #> Code_Target.set_printings (Type_Constructor ("fun",
     [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy (
         print_typ (INFX (1, X)) ty1,
diff -r 626d8f08d479 -r 0940309ed8f1 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_ml.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -14,6 +14,7 @@
 structure Code_ML : CODE_ML =
 struct
 
+open Basic_Code_Symbol;
 open Basic_Code_Thingol;
 open Code_Printer;
 
@@ -36,7 +37,7 @@
 datatype ml_stmt =
     ML_Exc of string * (typscheme * int)
   | ML_Val of ml_binding
-  | ML_Funs of ml_binding list * Code_Symbol.symbol list
+  | ML_Funs of ml_binding list * Code_Symbol.T list
   | ML_Datas of (string * (vname list * ((string * vname list) * itype list) list)) list
   | ML_Class of string * (vname * ((class * class) list * (string * itype) list));
 
@@ -53,21 +54,21 @@
 
 fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   let
-    val deresolve_const = deresolve o Code_Symbol.Constant;
-    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
-    val deresolve_class = deresolve o Code_Symbol.Type_Class;
-    val deresolve_classrel = deresolve o Code_Symbol.Class_Relation;
-    val deresolve_inst = deresolve o Code_Symbol.Class_Instance;
+    val deresolve_const = deresolve o Constant;
+    val deresolve_tyco = deresolve o Type_Constructor;
+    val deresolve_class = deresolve o Type_Class;
+    val deresolve_classrel = deresolve o Class_Relation;
+    val deresolve_inst = deresolve o Class_Instance;
     fun print_tyco_expr (sym, []) = (str o deresolve) sym
       | print_tyco_expr (sym, [ty]) =
           concat [print_typ BR ty, (str o deresolve) sym]
       | print_tyco_expr (sym, tys) =
           concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
     and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
-         of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys)
+         of NONE => print_tyco_expr (Type_Constructor tyco, tys)
           | SOME (_, print) => print print_typ fxy tys)
       | print_typ fxy (ITyVar v) = str ("'" ^ v);
-    fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]);
+    fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
     fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
       (map_filter (fn (v, sort) =>
         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
@@ -81,7 +82,7 @@
       print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)
     and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
           ((str o deresolve_inst) inst ::
-            (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
+            (if is_pseudo_fun (Class_Instance inst) then [str "()"]
             else map_filter (print_dicts is_pseudo_fun BR) dss))
       | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
           [str (if k = 1 then first_upper v ^ "_"
@@ -110,7 +111,7 @@
           in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
       | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
           (case Code_Thingol.unfold_const_app (#primitive case_expr)
-           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
+           of SOME (app as ({ sym = Constant const, ... }, _)) =>
                 if is_none (const_syntax const)
                 then print_case is_pseudo_fun some_thm vars fxy case_expr
                 else print_app is_pseudo_fun some_thm vars fxy app
@@ -174,7 +175,7 @@
       in
         concat (
           str definer
-          :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
+          :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
           :: str "="
           :: separate (str "|") (map print_co cos)
         )
@@ -195,7 +196,7 @@
               in
                 concat (
                   prolog
-                  :: (if is_pseudo_fun (Code_Symbol.Constant const) then [str "()"]
+                  :: (if is_pseudo_fun (Constant const) then [str "()"]
                       else print_dict_args vs
                         @ map (print_term is_pseudo_fun some_thm vars BR) ts)
                   @ str "="
@@ -205,7 +206,7 @@
             val shift = if null eqs then I else
               map (Pretty.block o single o Pretty.block o single);
           in pair
-            (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
+            (print_val_decl print_typscheme (Constant const, vs_ty))
             ((Pretty.block o Pretty.fbreaks o shift) (
               print_eqn definer eq
               :: map (print_eqn "|") eqs
@@ -228,11 +229,11 @@
               ];
           in pair
             (print_val_decl print_dicttypscheme
-              (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
+              (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
             (concat (
               str definer
               :: (str o deresolve_inst) inst
-              :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
+              :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
                   else print_dict_args vs)
               @ str "="
               :: enum "," "{" "}"
@@ -243,7 +244,7 @@
             ))
           end;
     fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
-          [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
+          [print_val_decl print_typscheme (Constant const, vs_ty)]
           ((semicolon o map str) (
             (if n = 0 then "val" else "fun")
             :: deresolve_const const
@@ -279,7 +280,7 @@
           end
      | print_stmt (ML_Datas [(tyco, (vs, []))]) =
           let
-            val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
+            val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
           in
             pair
             [concat [str "type", ty_p]]
@@ -301,7 +302,7 @@
               (map str ["val", s, "=", "#" ^ s, ":"] @| p);
             fun print_super_class_decl (classrel as (_, super_class)) =
               print_val_decl print_dicttypscheme
-                (Code_Symbol.Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
+                (Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
             fun print_super_class_field (classrel as (_, super_class)) =
               print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
             fun print_super_class_proj (classrel as (_, super_class)) =
@@ -309,7 +310,7 @@
                 (print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));
             fun print_classparam_decl (classparam, ty) =
               print_val_decl print_typscheme
-                (Code_Symbol.Constant classparam, ([(v, [class])], ty));
+                (Constant classparam, ([(v, [class])], ty));
             fun print_classparam_field (classparam, ty) =
               print_field (deresolve_const classparam) (print_typ NOBR ty);
             fun print_classparam_proj (classparam, ty) =
@@ -359,21 +360,21 @@
 
 fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   let
-    val deresolve_const = deresolve o Code_Symbol.Constant;
-    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
-    val deresolve_class = deresolve o Code_Symbol.Type_Class;
-    val deresolve_classrel = deresolve o Code_Symbol.Class_Relation;
-    val deresolve_inst = deresolve o Code_Symbol.Class_Instance;
+    val deresolve_const = deresolve o Constant;
+    val deresolve_tyco = deresolve o Type_Constructor;
+    val deresolve_class = deresolve o Type_Class;
+    val deresolve_classrel = deresolve o Class_Relation;
+    val deresolve_inst = deresolve o Class_Instance;
     fun print_tyco_expr (sym, []) = (str o deresolve) sym
       | print_tyco_expr (sym, [ty]) =
           concat [print_typ BR ty, (str o deresolve) sym]
       | print_tyco_expr (sym, tys) =
           concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
     and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
-         of NONE => print_tyco_expr (Code_Symbol.Type_Constructor tyco, tys)
+         of NONE => print_tyco_expr (Type_Constructor tyco, tys)
           | SOME (_, print) => print print_typ fxy tys)
       | print_typ fxy (ITyVar v) = str ("'" ^ v);
-    fun print_dicttyp (class, ty) = print_tyco_expr (Code_Symbol.Type_Class class, [ty]);
+    fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
     fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
       (map_filter (fn (v, sort) =>
         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
@@ -386,7 +387,7 @@
       |> print_classrels classrels
     and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
           brackify BR ((str o deresolve_inst) inst ::
-            (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
+            (if is_pseudo_fun (Class_Instance inst) then [str "()"]
             else map_filter (print_dicts is_pseudo_fun BR) dss))
       | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
           str (if k = 1 then "_" ^ first_upper v
@@ -412,7 +413,7 @@
           in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
       | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
           (case Code_Thingol.unfold_const_app (#primitive case_expr)
-           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
+           of SOME (app as ({ sym = Constant const, ... }, _)) =>
                 if is_none (const_syntax const)
                 then print_case is_pseudo_fun some_thm vars fxy case_expr
                 else print_app is_pseudo_fun some_thm vars fxy app
@@ -471,7 +472,7 @@
       in
         concat (
           str definer
-          :: print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs)
+          :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
           :: str "="
           :: separate (str "|") (map print_co cos)
         )
@@ -544,11 +545,11 @@
               concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
                 else (concat o map str) [definer, deresolve_const const];
           in pair
-            (print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty))
+            (print_val_decl print_typscheme (Constant const, vs_ty))
             (concat (
               prolog
               :: print_dict_args vs
-              @| print_eqns (is_pseudo_fun (Code_Symbol.Constant const)) eqs
+              @| print_eqns (is_pseudo_fun (Constant const)) eqs
             ))
           end
       | print_def is_pseudo_fun _ definer
@@ -568,11 +569,11 @@
               ];
           in pair
             (print_val_decl print_dicttypscheme
-              (Code_Symbol.Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
+              (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
             (concat (
               str definer
               :: (str o deresolve_inst) inst
-              :: (if is_pseudo_fun (Code_Symbol.Class_Instance inst) then [str "()"]
+              :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
                   else print_dict_args vs)
               @ str "="
               @@ brackets [
@@ -584,7 +585,7 @@
             ))
           end;
      fun print_stmt (ML_Exc (const, (vs_ty, n))) = pair
-          [print_val_decl print_typscheme (Code_Symbol.Constant const, vs_ty)]
+          [print_val_decl print_typscheme (Constant const, vs_ty)]
           ((doublesemicolon o map str) (
             "let"
             :: deresolve_const const
@@ -619,7 +620,7 @@
           end
      | print_stmt (ML_Datas [(tyco, (vs, []))]) =
           let
-            val ty_p = print_tyco_expr (Code_Symbol.Type_Constructor tyco, map ITyVar vs);
+            val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
           in
             pair
             [concat [str "type", ty_p]]
@@ -641,7 +642,7 @@
               print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
             fun print_classparam_decl (classparam, ty) =
               print_val_decl print_typscheme
-                (Code_Symbol.Constant classparam, ([(v, [class])], ty));
+                (Constant classparam, ([(v, [class])], ty));
             fun print_classparam_field (classparam, ty) =
               print_field (deresolve_const classparam) (print_typ NOBR ty);
             val w = "_" ^ first_upper v;
@@ -724,7 +725,7 @@
       | namify_stmt (Code_Thingol.Classrel _) = namify_const false
       | namify_stmt (Code_Thingol.Classparam _) = namify_const false
       | namify_stmt (Code_Thingol.Classinst _) = namify_const false;
-    fun ml_binding_of_stmt (sym as Code_Symbol.Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
+    fun ml_binding_of_stmt (sym as Constant const, Code_Thingol.Fun ((tysm as (vs, ty), raw_eqs), _)) =
           let
             val eqs = filter (snd o snd) raw_eqs;
             val (eqs', some_sym) = if null (filter_out (null o snd) vs) then case eqs
@@ -734,7 +735,7 @@
                 | _ => (eqs, NONE)
               else (eqs, NONE)
           in (ML_Function (const, (tysm, eqs')), some_sym) end
-      | ml_binding_of_stmt (sym as Code_Symbol.Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
+      | ml_binding_of_stmt (sym as Class_Instance inst, Code_Thingol.Classinst (stmt as { vs, ... })) =
           (ML_Instance (inst, stmt), if forall (null o snd) vs then SOME (sym, false) else NONE)
       | ml_binding_of_stmt (sym, _) =
           error ("Binding block containing illegal statement: " ^ 
@@ -755,10 +756,10 @@
       (ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst)))
     fun modify_datatypes stmts = single (SOME
       (ML_Datas (map_filter
-        (fn (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
+        (fn (Type_Constructor tyco, Code_Thingol.Datatype stmt) => SOME (tyco, stmt) | _ => NONE) stmts)))
     fun modify_class stmts = single (SOME
       (ML_Class (the_single (map_filter
-        (fn (Code_Symbol.Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
+        (fn (Type_Class class, Code_Thingol.Class stmt) => SOME (class, stmt) | _ => NONE) stmts))))
     fun modify_stmts ([stmt as (_, stmt' as Code_Thingol.Fun _)]) =
           if Code_Thingol.is_case stmt' then [] else [modify_fun stmt]
       | modify_stmts ((stmts as (_, Code_Thingol.Fun _) :: _)) =
@@ -850,7 +851,7 @@
       check = { env_var = "ISABELLE_OCAML",
         make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
         make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
-  #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
+  #> Code_Target.set_printings (Type_Constructor ("fun",
     [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   #> fold (Code_Target.add_reserved target_SML)
diff -r 626d8f08d479 -r 0940309ed8f1 src/Tools/Code/code_namespace.ML
--- a/src/Tools/Code/code_namespace.ML	Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_namespace.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -13,7 +13,7 @@
     namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a,
     modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option }
       -> Code_Thingol.program
-      -> { deresolver: string -> Code_Symbol.symbol -> string,
+      -> { deresolver: string -> Code_Symbol.T -> string,
            flat_program: flat_program }
 
   datatype ('a, 'b) node =
@@ -26,13 +26,13 @@
     reserved: Name.context, identifiers: Code_Target.identifier_data,
     empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
     namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
-    cyclic_modules: bool, empty_data: 'b, memorize_data: Code_Symbol.symbol -> 'b -> 'b,
-    modify_stmts: (Code_Symbol.symbol * Code_Thingol.stmt) list -> 'a option list }
+    cyclic_modules: bool, empty_data: 'b, memorize_data: Code_Symbol.T -> 'b -> 'b,
+    modify_stmts: (Code_Symbol.T * Code_Thingol.stmt) list -> 'a option list }
       -> Code_Thingol.program
-      -> { deresolver: string list -> Code_Symbol.symbol -> string,
+      -> { deresolver: string list -> Code_Symbol.T -> string,
            hierarchical_program: ('a, 'b) hierarchical_program }
   val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c,
-    print_stmt: string list -> Code_Symbol.symbol * 'a -> 'c,
+    print_stmt: string list -> Code_Symbol.T * 'a -> 'c,
     lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c }
       -> ('a, 'b) hierarchical_program -> 'c list
 end;
@@ -48,7 +48,7 @@
 
 fun force_identifier ctxt fragments_tab force_module identifiers sym =
   case lookup_identifier identifiers sym of
-      NONE => ((the o Symtab.lookup fragments_tab o Code_Symbol.namespace_prefix ctxt) sym, Code_Symbol.base_name sym)
+      NONE => ((the o Symtab.lookup fragments_tab o Code_Symbol.default_prefix ctxt) sym, Code_Symbol.default_base sym)
     | SOME prefix_name => if null force_module then prefix_name
         else (force_module, snd prefix_name);
 
@@ -57,7 +57,7 @@
     fun alias_fragments name = case module_identifiers name
      of SOME name' => Long_Name.explode name'
       | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name);
-    val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.namespace_prefix ctxt o fst) program [];
+    val module_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) program [];
   in
     fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))
       module_names Symtab.empty
@@ -66,7 +66,7 @@
 
 (** flat program structure **)
 
-type flat_program = ((string * Code_Thingol.stmt option) Code_Symbol.Graph.T * (string * Code_Symbol.symbol list) list) Graph.T;
+type flat_program = ((string * Code_Thingol.stmt option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
 
 fun flat_program ctxt { module_prefix, module_name, reserved,
     identifiers, empty_nsp, namify_stmt, modify_stmt } program =
diff -r 626d8f08d479 -r 0940309ed8f1 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_printer.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -25,8 +25,8 @@
   val semicolon: Pretty.T list -> Pretty.T
   val doublesemicolon: Pretty.T list -> Pretty.T
   val indent: int -> Pretty.T -> Pretty.T
-  val markup_stmt: Code_Symbol.symbol -> Pretty.T -> Pretty.T
-  val format: Code_Symbol.symbol list -> int -> Pretty.T -> string
+  val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T
+  val format: Code_Symbol.T list -> int -> Pretty.T -> string
 
   val first_upper: string -> string
   val first_lower: string -> string
@@ -36,7 +36,7 @@
   val lookup_var: var_ctxt -> string -> string
   val intro_base_names: (string -> bool) -> (string -> string)
     -> string list -> var_ctxt -> var_ctxt
-  val intro_base_names_for: (string -> bool) -> (Code_Symbol.symbol -> string)
+  val intro_base_names_for: (string -> bool) -> (Code_Symbol.T -> string)
     -> iterm list -> var_ctxt -> var_ctxt
   val aux_params: var_ctxt -> iterm list list -> string list
 
@@ -94,6 +94,7 @@
 structure Code_Printer : CODE_PRINTER =
 struct
 
+open Basic_Code_Symbol;
 open Code_Thingol;
 
 (** generic nonsense *)
@@ -200,7 +201,7 @@
 fun intro_base_names_for no_syntax deresolve ts =
   []
   |> fold Code_Thingol.add_constsyms ts 
-  |> intro_base_names (fn Code_Symbol.Constant const => no_syntax const | _ => true) deresolve;
+  |> intro_base_names (fn Constant const => no_syntax const | _ => true) deresolve;
 
 
 (** pretty literals **)
@@ -313,7 +314,7 @@
 fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
     (app as ({ sym, dom, ... }, ts)) =
   case sym of
-    Code_Symbol.Constant const => (case const_syntax const of
+    Constant const => (case const_syntax const of
       NONE => brackify fxy (print_app_expr some_thm vars app)
     | SOME (Plain_const_syntax (_, s)) =>
         brackify fxy (str s :: map (print_term some_thm vars BR) ts)
diff -r 626d8f08d479 -r 0940309ed8f1 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -36,6 +36,7 @@
 structure Code_Runtime : CODE_RUNTIME =
 struct
 
+open Basic_Code_Symbol;
 open Basic_Code_Thingol;
 
 (** evaluation **)
@@ -53,9 +54,9 @@
 
 val _ = Theory.setup
   (Code_Target.extend_target (target, (Code_ML.target_SML, I))
-  #> Code_Target.set_printings (Code_Symbol.Type_Constructor (@{type_name prop},
+  #> Code_Target.set_printings (Type_Constructor (@{type_name prop},
     [(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
-  #> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Code_Generator.holds},
+  #> Code_Target.set_printings (Constant (@{const_name Code_Generator.holds},
     [(target, SOME (Code_Printer.plain_const_syntax s_Holds))]))
   #> Code_Target.add_reserved target this
   #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]);
@@ -92,7 +93,7 @@
   |> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
 
 fun obtain_evaluator' thy some_target program =
-  obtain_evaluator thy some_target program o map Code_Symbol.Constant;
+  obtain_evaluator thy some_target program o map Constant;
 
 fun evaluation cookie thy evaluator vs_t args =
   let
@@ -198,7 +199,7 @@
     val program = Code_Thingol.consts_program thy false consts;
     val (ml_modules, target_names) =
       Code_Target.produce_code_for thy
-        target NONE module_name [] program (map Code_Symbol.Constant consts @ map Code_Symbol.Type_Constructor tycos);
+        target NONE module_name [] program (map Constant consts @ map Type_Constructor tycos);
     val ml_code = space_implode "\n\n" (map snd ml_modules);
     val (consts', tycos') = chop (length consts) target_names;
     val consts_map = map2 (fn const =>
@@ -292,7 +293,7 @@
           Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
   in
     thy
-    |> Code_Target.set_printings (Code_Symbol.Type_Constructor (tyco, [(target, SOME (k, pr))]))
+    |> Code_Target.set_printings (Type_Constructor (tyco, [(target, SOME (k, pr))]))
   end;
 
 fun add_eval_constr (const, const') thy =
@@ -302,11 +303,11 @@
       (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
   in
     thy
-    |> Code_Target.set_printings (Code_Symbol.Constant (const,
+    |> Code_Target.set_printings (Constant (const,
       [(target, SOME (Code_Printer.simple_const_syntax (k, pr)))]))
   end;
 
-fun add_eval_const (const, const') = Code_Target.set_printings (Code_Symbol.Constant
+fun add_eval_const (const, const') = Code_Target.set_printings (Constant
   (const, [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')))]));
 
 fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy =
@@ -437,7 +438,7 @@
   |> Code_Target.add_reserved target ml_name
   |> Specification.axiomatization [(b, SOME T, NoSyn)] []
   |-> (fn ([Const (const, _)], _) =>
-    Code_Target.set_printings (Code_Symbol.Constant (const,
+    Code_Target.set_printings (Constant (const,
       [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
   #> tap (fn thy => Code_Target.produce_code thy [const] target NONE structure_generated []));
 
diff -r 626d8f08d479 -r 0940309ed8f1 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_scala.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -15,6 +15,7 @@
 
 val target = "Scala";
 
+open Basic_Code_Symbol;
 open Basic_Code_Thingol;
 open Code_Printer;
 
@@ -27,18 +28,18 @@
 fun print_scala_stmt tyco_syntax const_syntax reserved
     args_num is_constr (deresolve, deresolve_full) =
   let
-    val deresolve_const = deresolve o Code_Symbol.Constant;
-    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
-    val deresolve_class = deresolve o Code_Symbol.Type_Class;
+    val deresolve_const = deresolve o Constant;
+    val deresolve_tyco = deresolve o Type_Constructor;
+    val deresolve_class = deresolve o Type_Class;
     fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
     fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
     fun print_tyco_expr tyvars fxy (sym, tys) = applify "[" "]"
           (print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys
     and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
-         of NONE => print_tyco_expr tyvars fxy (Code_Symbol.Type_Constructor tyco, tys)
+         of NONE => print_tyco_expr tyvars fxy (Type_Constructor tyco, tys)
           | SOME (_, print) => print (print_typ tyvars) fxy tys)
       | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
-    fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Code_Symbol.Type_Class class, [ty]);
+    fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Type_Class class, [ty]);
     fun print_tupled_typ tyvars ([], ty) =
           print_typ tyvars NOBR ty
       | print_tupled_typ tyvars ([ty1], ty2) =
@@ -70,7 +71,7 @@
           end
       | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) =
           (case Code_Thingol.unfold_const_app (#primitive case_expr)
-           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
+           of SOME (app as ({ sym = Constant const, ... }, _)) =>
                 if is_none (const_syntax const)
                 then print_case tyvars some_thm vars fxy case_expr
                 else print_app tyvars is_pat some_thm vars fxy app
@@ -81,7 +82,7 @@
         val k = length ts;
         val typargs' = if is_pat then [] else typargs;
         val syntax = case sym of
-            Code_Symbol.Constant const => const_syntax const
+            Constant const => const_syntax const
           | _ => NONE;
         val (l, print') = case syntax of
             NONE => (args_num sym, fn fxy => fn ts => gen_applify (is_constr sym) "(" ")"
@@ -151,7 +152,7 @@
     fun print_defhead tyvars vars const vs params tys ty =
       Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
         constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
-          NOBR (print_context tyvars vs (Code_Symbol.Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
+          NOBR (print_context tyvars vs (Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
             str " ="];
     fun print_def const (vs, ty) [] =
           let
@@ -204,10 +205,10 @@
                 str "match", str "{"], str "}")
               (map print_clause eqs)
           end;
-    val print_method = str o Library.enclose "`" "`" o deresolve_full o Code_Symbol.Constant;
-    fun print_stmt (Code_Symbol.Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
+    val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant;
+    fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
           print_def const (vs, ty) (filter (snd o snd) raw_eqs)
-      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) =
+      | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) =
           let
             val tyvars = intro_tyvars (map (rpair []) vs) reserved;
             fun print_co ((co, vs_args), tys) =
@@ -224,7 +225,7 @@
               NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
                 :: map print_co cos)
           end
-      | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
+      | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
           let
             val tyvars = intro_tyvars [(v, [class])] reserved;
             fun add_typarg s = Pretty.block
@@ -349,12 +350,12 @@
       scala_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
 
     (* print statements *)
-    fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Code_Symbol.Type_Constructor tyco)
+    fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Type_Constructor tyco)
      of Code_Thingol.Datatype (_, constrs) =>
           the (AList.lookup (op = o apsnd fst) constrs constr);
-    fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Code_Symbol.Type_Class class)
+    fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Type_Class class)
      of Code_Thingol.Class (_, (_, classparams)) => classparams;
-    fun args_num (sym as Code_Symbol.Constant const) = case Code_Symbol.Graph.get_node program sym
+    fun args_num (sym as Constant const) = case Code_Symbol.Graph.get_node program sym
      of Code_Thingol.Fun (((_, ty), []), _) =>
           (length o fst o Code_Thingol.unfold_fun) ty
       | Code_Thingol.Fun ((_, ((ts, _), _) :: _), _) => length ts
@@ -422,7 +423,7 @@
         make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
         make_command = fn _ =>
           "env JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' \"$SCALA_HOME/bin/scalac\" ROOT.scala" } })
-  #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
+  #> Code_Target.set_printings (Type_Constructor ("fun",
     [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy (
         print_typ BR ty1 (*product type vs. tupled arguments!*),
diff -r 626d8f08d479 -r 0940309ed8f1 src/Tools/Code/code_symbol.ML
--- a/src/Tools/Code/code_symbol.ML	Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_symbol.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -5,20 +5,25 @@
 class relations, class instances, modules.
 *)
 
-signature CODE_SYMBOL =
+signature BASIC_CODE_SYMBOL =
 sig
   datatype ('a, 'b, 'c, 'd, 'e, 'f) attr =
     Constant of 'a | Type_Constructor of 'b | Type_Class of 'c |
     Class_Relation of 'd  | Class_Instance of 'e | Module of 'f
-  type symbol = (string, string, class, class * class, string * class, string) attr
-  structure Table: TABLE;
-  structure Graph: GRAPH;
-  val namespace_prefix: Proof.context -> symbol -> string
-  val base_name: symbol -> string
-  val quote: Proof.context -> symbol -> string
-  val marker: symbol -> string
-  val value: symbol
-  val is_value: symbol -> bool
+end
+
+signature CODE_SYMBOL =
+sig
+  include BASIC_CODE_SYMBOL
+  type T = (string, string, class, class * class, string * class, string) attr
+  structure Table: TABLE
+  structure Graph: GRAPH
+  val default_base: T -> string
+  val default_prefix: Proof.context -> T -> string
+  val quote: Proof.context -> T -> string
+  val marker: T -> string
+  val value: T
+  val is_value: T -> bool
   val map_attr: ('a -> 'g) -> ('b -> 'h) -> ('c -> 'i) -> ('d -> 'j) -> ('e -> 'k) -> ('f -> 'l)
     -> ('a, 'b, 'c, 'd, 'e, 'f) attr -> ('g, 'h, 'i, 'j, 'k, 'l) attr
   val maps_attr: ('a -> 'g list) -> ('b -> 'h list)
@@ -40,8 +45,8 @@
   val lookup_class_relation_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> class * class -> 'd option
   val lookup_class_instance_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string * class -> 'e option
   val lookup_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> string -> 'f option
-  val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> symbol -> 'a option
-  val symbols_of: ('a, 'b, 'c, 'd, 'e, 'f) data -> symbol list
+  val lookup: ('a, 'a, 'a, 'a, 'a, 'a) data -> T -> 'a option
+  val symbols_of: ('a, 'b, 'c, 'd, 'e, 'f) data -> T list
   val dest_module_data: ('a, 'b, 'c, 'd, 'e, 'f) data -> (string * 'f) list
 end;
 
@@ -53,7 +58,7 @@
 datatype ('a, 'b, 'c, 'd, 'e, 'f) attr =
   Constant of 'a | Type_Constructor of 'b | Type_Class of 'c | Class_Relation of 'd  | Class_Instance of 'e | Module of 'f;
 
-type symbol = (string, string, class, string * class, class * class, string) attr;
+type T = (string, string, class, string * class, class * class, string) attr;
 
 fun symbol_ord (Constant c1, Constant c2) = fast_string_ord (c1, c2)
   | symbol_ord (Constant _, _) = GREATER
@@ -74,8 +79,24 @@
   | symbol_ord (_, Class_Instance _) = LESS
   | symbol_ord (Module name1, Module name2) = fast_string_ord (name1, name2);
 
-structure Table = Table(type key = symbol val ord = symbol_ord);
-structure Graph = Graph(type key = symbol val ord = symbol_ord);
+structure Table = Table(type key = T val ord = symbol_ord);
+structure Graph = Graph(type key = T val ord = symbol_ord);
+
+local
+  val base = Name.desymbolize false o Long_Name.base_name;
+  fun base_rel (x, y) = base y ^ "_" ^ base x;
+in
+
+fun default_base (Constant "") = "value"
+  | default_base (Constant "==>") = "follows"
+  | default_base (Constant "==") = "meta_eq"
+  | default_base (Constant c) = base c
+  | default_base (Type_Constructor tyco) = base tyco
+  | default_base (Type_Class class) = base class
+  | default_base (Class_Relation classrel) = base_rel classrel
+  | default_base (Class_Instance inst) = base_rel inst;
+
+end;
 
 local
   fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
@@ -94,29 +115,16 @@
     | prefix thy (Type_Class class) = thyname_of_class thy class
     | prefix thy (Class_Relation (class, _)) = thyname_of_class thy class
     | prefix thy (Class_Instance inst) = thyname_of_instance thy inst;
-  val base = Name.desymbolize false o Long_Name.base_name;
-  fun base_rel (x, y) = base y ^ "_" ^ base x;
 in
 
-fun base_name (Constant "") = "value"
-  | base_name (Constant "==>") = "follows"
-  | base_name (Constant "==") = "meta_eq"
-  | base_name (Constant c) = base c
-  | base_name (Type_Constructor tyco) = base tyco
-  | base_name (Type_Class class) = base class
-  | base_name (Class_Relation classrel) = base_rel classrel
-  | base_name (Class_Instance inst) = base_rel inst;
+fun default_prefix ctxt = prefix (Proof_Context.theory_of ctxt);
 
-fun namespace_prefix ctxt = prefix (Proof_Context.theory_of ctxt);
-
-fun default_name ctxt sym = (namespace_prefix ctxt sym, base_name sym);
+end;
 
 val value = Constant "";
 fun is_value (Constant "") = true
   | is_value _ = false;
 
-end;
-
 fun quote ctxt (Constant c) = Library.quote (Code.string_of_const (Proof_Context.theory_of ctxt) c)
   | quote ctxt (Type_Constructor tyco) = "type " ^ Library.quote (Proof_Context.extern_type ctxt tyco)
   | quote ctxt (Type_Class class) = "class " ^ Library.quote (Proof_Context.extern_class ctxt class)
@@ -216,3 +224,6 @@
 fun dest_module_data x = (Symtab.dest o #module o dest_data) x;
 
 end;
+
+
+structure Basic_Code_Symbol: BASIC_CODE_SYMBOL = Code_Symbol;
diff -r 626d8f08d479 -r 0940309ed8f1 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -11,26 +11,26 @@
   val read_const_exprs: theory -> string list -> string list
 
   val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
-    -> Code_Thingol.program -> Code_Symbol.symbol list -> unit
+    -> Code_Thingol.program -> Code_Symbol.T list -> unit
   val produce_code_for: theory -> string -> int option -> string -> Token.T list
-    -> Code_Thingol.program -> Code_Symbol.symbol list -> (string * string) list * string option list
+    -> Code_Thingol.program -> Code_Symbol.T list -> (string * string) list * string option list
   val present_code_for: theory -> string -> int option -> string -> Token.T list
-    -> Code_Thingol.program -> Code_Symbol.symbol list * Code_Symbol.symbol list -> string
+    -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string
   val check_code_for: theory -> string -> bool -> Token.T list
-    -> Code_Thingol.program -> Code_Symbol.symbol list -> unit
+    -> Code_Thingol.program -> Code_Symbol.T list -> unit
 
   val export_code: theory -> string list
     -> (((string * string) * Path.T option) * Token.T list) list -> unit
   val produce_code: theory -> string list
     -> string -> int option -> string -> Token.T list -> (string * string) list * string option list
-  val present_code: theory -> string list -> Code_Symbol.symbol list
+  val present_code: theory -> string list -> Code_Symbol.T list
     -> string -> int option -> string -> Token.T list -> string
   val check_code: theory -> string list
     -> ((string * bool) * Token.T list) list -> unit
 
   val generatedN: string
   val evaluator: theory -> string -> Code_Thingol.program
-    -> Code_Symbol.symbol list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
+    -> Code_Symbol.T list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
     -> (string * string) list * string
 
   type serializer
@@ -46,7 +46,7 @@
   type serialization
   val parse_args: 'a parser -> Token.T list -> 'a
   val serialization: (int -> Path.T option -> 'a -> unit)
-    -> (Code_Symbol.symbol list -> int -> 'a -> (string * string) list * (Code_Symbol.symbol -> string option))
+    -> (Code_Symbol.T list -> int -> 'a -> (string * string) list * (Code_Symbol.T -> string option))
     -> 'a -> serialization
   val set_default_code_width: int -> theory -> theory
 
@@ -73,6 +73,7 @@
 structure Code_Target : CODE_TARGET =
 struct
 
+open Basic_Code_Symbol;
 open Basic_Code_Thingol;
 
 type literals = Code_Printer.literals;
@@ -154,8 +155,8 @@
 
 (* serialization: abstract nonsense to cover different destinies for generated code *)
 
-datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.symbol list;
-type serialization = int -> destination -> ((string * string) list * (Code_Symbol.symbol -> string option)) option;
+datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.T list;
+type serialization = int -> destination -> ((string * string) list * (Code_Symbol.T -> string option)) option;
 
 fun serialization output _ content width (Export some_path) =
       (output width some_path content; NONE)
@@ -345,7 +346,7 @@
     val syms_hidden = Code_Symbol.symbols_of printings;
     val (syms_all, program) = project_program thy syms_hidden syms proto_program;
     fun select_include (name, (content, cs)) =
-      if null cs orelse exists (fn c => member (op =) syms_all (Code_Symbol.Constant c)) cs
+      if null cs orelse exists (fn c => member (op =) syms_all (Constant c)) cs
       then SOME (name, content) else NONE;
     val includes = map_filter select_include (Code_Symbol.dest_module_data printings);
   in
@@ -471,7 +472,7 @@
   let
     val program = Code_Thingol.consts_program thy false cs;
     val _ = map (fn (((target, module_name), some_path), args) =>
-      export_code_for thy some_path target NONE module_name args program (map Code_Symbol.Constant cs)) seris;
+      export_code_for thy some_path target NONE module_name args program (map Constant cs)) seris;
   in () end;
 
 fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs)
@@ -480,18 +481,18 @@
 fun produce_code thy cs target some_width some_module_name args =
   let
     val program = Code_Thingol.consts_program thy false cs;
-  in produce_code_for thy target some_width some_module_name args program (map Code_Symbol.Constant cs) end;
+  in produce_code_for thy target some_width some_module_name args program (map Constant cs) end;
 
 fun present_code thy cs syms target some_width some_module_name args =
   let
     val program = Code_Thingol.consts_program thy false cs;
-  in present_code_for thy target some_width some_module_name args program (map Code_Symbol.Constant cs, syms) end;
+  in present_code_for thy target some_width some_module_name args program (map Constant cs, syms) end;
 
 fun check_code thy cs seris =
   let
     val program = Code_Thingol.consts_program thy false cs;
     val _ = map (fn ((target, strict), args) =>
-      check_code_for thy target strict args program (map Code_Symbol.Constant cs)) seris;
+      check_code_for thy target strict args program (map Constant cs)) seris;
   in () end;
 
 fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;
@@ -506,17 +507,17 @@
   >> (fn xs => fn thy => map (mark_symbol o internalize thy) xs);
 
 val parse_consts = parse_names "consts" Args.term
-  Code.check_const Code_Symbol.Constant;
+  Code.check_const Constant;
 
 val parse_types = parse_names "types" (Scan.lift Args.name)
-  Sign.intern_type Code_Symbol.Type_Constructor;
+  Sign.intern_type Type_Constructor;
 
 val parse_classes = parse_names "classes" (Scan.lift Args.name)
-  Sign.intern_class Code_Symbol.Type_Class;
+  Sign.intern_class Type_Class;
 
 val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
   (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class))
-    Code_Symbol.Class_Instance;
+    Class_Instance;
 
 in
 
@@ -630,19 +631,19 @@
   in set_printing (target, Symbol (x, Option.map (prep_syn thy target x) some_raw_syn)) thy end;
 
 fun gen_add_const_syntax prep_const =
-  gen_add_syntax Code_Symbol.Constant prep_const check_const_syntax;
+  gen_add_syntax Constant prep_const check_const_syntax;
 
 fun gen_add_tyco_syntax prep_tyco =
-  gen_add_syntax Code_Symbol.Type_Constructor prep_tyco check_tyco_syntax;
+  gen_add_syntax Type_Constructor prep_tyco check_tyco_syntax;
 
 fun gen_add_class_syntax prep_class =
-  gen_add_syntax Code_Symbol.Type_Class prep_class ((K o K o K) I);
+  gen_add_syntax Type_Class prep_class ((K o K o K) I);
 
 fun gen_add_instance_syntax prep_inst =
-  gen_add_syntax Code_Symbol.Class_Instance prep_inst ((K o K o K) I);
+  gen_add_syntax Class_Instance prep_inst ((K o K o K) I);
 
 fun gen_add_include prep_const target (name, some_content) thy =
-  gen_add_syntax Code_Symbol.Module (K I)
+  gen_add_syntax Module (K I)
     (fn thy => fn _ => fn _ => fn (raw_content, raw_cs) => (Code_Printer.str raw_content, map (prep_const thy) raw_cs))
     target name some_content thy;
 
@@ -693,15 +694,15 @@
 
 fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
   parse_single_symbol_pragma @{keyword "constant"} Parse.term parse_const
-    >> Code_Symbol.Constant
+    >> Constant
   || parse_single_symbol_pragma @{keyword "type_constructor"} Parse.type_const parse_tyco
-    >> Code_Symbol.Type_Constructor
+    >> Type_Constructor
   || parse_single_symbol_pragma @{keyword "type_class"} Parse.class parse_class
-    >> Code_Symbol.Type_Class
+    >> Type_Class
   || parse_single_symbol_pragma @{keyword "class_relation"} parse_classrel_ident parse_classrel
-    >> Code_Symbol.Class_Relation
+    >> Class_Relation
   || parse_single_symbol_pragma @{keyword "class_instance"} parse_inst_ident parse_inst
-    >> Code_Symbol.Class_Instance
+    >> Class_Instance
   || parse_single_symbol_pragma @{keyword "code_module"} Parse.name parse_module
     >> Code_Symbol.Module;
 
diff -r 626d8f08d479 -r 0940309ed8f1 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -23,7 +23,7 @@
   datatype itype =
       `%% of string * itype list
     | ITyVar of vname;
-  type const = { sym: Code_Symbol.symbol, typargs: itype list, dicts: dict list list,
+  type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
     dom: itype list, range: itype, annotate: bool };
   datatype iterm =
       IConst of const
@@ -55,7 +55,7 @@
   val is_IAbs: iterm -> bool
   val eta_expand: int -> const * iterm list -> iterm
   val contains_dict_var: iterm -> bool
-  val add_constsyms: iterm -> Code_Symbol.symbol list -> Code_Symbol.symbol list
+  val add_constsyms: iterm -> Code_Symbol.T list -> Code_Symbol.T list
   val add_tyconames: iterm -> string list -> string list
   val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
 
@@ -77,34 +77,36 @@
   val implemented_deps: program -> string list
   val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
   val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
-  val is_constr: program -> Code_Symbol.symbol -> bool
+  val is_constr: program -> Code_Symbol.T -> bool
   val is_case: stmt -> bool
   val group_stmts: theory -> program
-    -> ((Code_Symbol.symbol * stmt) list * (Code_Symbol.symbol * stmt) list
-      * ((Code_Symbol.symbol * stmt) list * (Code_Symbol.symbol * stmt) list)) list
+    -> ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list
+      * ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list
 
   val read_const_exprs: theory -> string list -> string list * string list
   val consts_program: theory -> bool -> string list -> program
   val dynamic_conv: theory -> (program
-    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> conv)
+    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
     -> conv
   val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (program
-    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> 'a)
+    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
     -> term -> 'a
   val static_conv: theory -> string list -> (program -> string list
-    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> conv)
+    -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
     -> conv
   val static_conv_simple: theory -> string list
     -> (program -> (string * sort) list -> term -> conv) -> conv
   val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
     (program -> string list
-      -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.symbol list -> 'a)
+      -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> 'a)
     -> term -> 'a
 end;
 
 structure Code_Thingol: CODE_THINGOL =
 struct
 
+open Basic_Code_Symbol;
+
 (** auxiliary **)
 
 fun unfoldl dest x =
@@ -147,7 +149,7 @@
     val ty3 = Library.foldr (op `->) (tys2, ty1);
   in (tys3, ty3) end;
 
-type const = { sym: Code_Symbol.symbol, typargs: itype list, dicts: dict list list,
+type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
   dom: itype list, range: itype, annotate: bool };
 
 datatype iterm =
@@ -286,12 +288,12 @@
 type program = stmt Code_Symbol.Graph.T;
 
 fun unimplemented program =
-  Code_Symbol.Graph.fold (fn (Code_Symbol.Constant c, (NoStmt, _)) => cons c | _ => I) program [];
+  Code_Symbol.Graph.fold (fn (Constant c, (NoStmt, _)) => cons c | _ => I) program [];
 
 fun implemented_deps program =
   Code_Symbol.Graph.keys program
-  |> subtract (op =) (Code_Symbol.Graph.all_preds program (map Code_Symbol.Constant (unimplemented program)))
-  |> map_filter (fn Code_Symbol.Constant c => SOME c | _ => NONE);
+  |> subtract (op =) (Code_Symbol.Graph.all_preds program (map Constant (unimplemented program)))
+  |> map_filter (fn Constant c => SOME c | _ => NONE);
 
 fun map_terms_bottom_up f (t as IConst _) = f t
   | map_terms_bottom_up f (t as IVar _) = f t
@@ -466,7 +468,7 @@
         ##>> pair (map (unprefix "'" o fst) vs)
         ##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
       #>> Datatype;
-  in ensure_stmt Code_Symbol.Type_Constructor stmt_datatype tyco end
+  in ensure_stmt Type_Constructor stmt_datatype tyco end
 and ensure_const thy algbr eqngr permissive c =
   let
     fun stmt_datatypecons tyco =
@@ -494,7 +496,7 @@
       | NONE => (case Axclass.class_of_param thy c
          of SOME class => stmt_classparam class
           | NONE => stmt_fun (Code_Preproc.cert eqngr c))
-  in ensure_stmt Code_Symbol.Constant stmt_const c end
+  in ensure_stmt Constant stmt_const c end
 and ensure_class thy (algbr as (_, algebra)) eqngr permissive class =
   let
     val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
@@ -505,14 +507,14 @@
       ##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
         ##>> translate_typ thy algbr eqngr permissive ty) cs
       #>> (fn info => Class (unprefix "'" Name.aT, info))
-  in ensure_stmt Code_Symbol.Type_Class stmt_class class end
+  in ensure_stmt Type_Class stmt_class class end
 and ensure_classrel thy algbr eqngr permissive (sub_class, super_class) =
   let
     val stmt_classrel =
       ensure_class thy algbr eqngr permissive sub_class
       ##>> ensure_class thy algbr eqngr permissive super_class
       #>> Classrel;
-  in ensure_stmt Code_Symbol.Class_Relation stmt_classrel (sub_class, super_class) end
+  in ensure_stmt Class_Relation stmt_classrel (sub_class, super_class) end
 and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (tyco, class) =
   let
     val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
@@ -552,7 +554,7 @@
       #>> (fn (((((class, tyco), vs), superinsts), inst_params), superinst_params) =>
           Classinst { class = class, tyco = tyco, vs = vs,
             superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params });
-  in ensure_stmt Code_Symbol.Class_Instance stmt_inst (tyco, class) end
+  in ensure_stmt Class_Instance stmt_inst (tyco, class) end
 and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
       pair (ITyVar (unprefix "'" v))
   | translate_typ thy algbr eqngr permissive (Type (tyco, tys)) =
@@ -604,7 +606,7 @@
     ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (typargs ~~ sorts)
     ##>> fold_map (translate_typ thy algbr eqngr permissive) (range :: dom)
     #>> (fn (((c, typargs), dss), range :: dom) =>
-      IConst { sym = Code_Symbol.Constant c, typargs = typargs, dicts = dss,
+      IConst { sym = Constant c, typargs = typargs, dicts = dss,
         dom = dom, range = range, annotate = annotate })
   end
 and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
@@ -629,7 +631,7 @@
       let
         fun collapse_clause vs_map ts body =
           case body
-           of IConst { sym = Code_Symbol.Constant c, ... } => if member (op =) undefineds c
+           of IConst { sym = Constant c, ... } => if member (op =) undefineds c
                 then []
                 else [(ts, body)]
             | ICase { term = IVar (SOME v), clauses = clauses, ... } =>
@@ -747,7 +749,7 @@
       if permissive then program
       else Code_Symbol.Graph.restrict
         (member (op =) (Code_Symbol.Graph.all_succs program
-          (map Code_Symbol.Constant consts))) program;
+          (map Constant consts))) program;
     fun generate_consts thy algebra eqngr =
       fold_map (ensure_const thy algebra eqngr permissive);
   in
@@ -766,7 +768,7 @@
     val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
       o dest_TFree))) t [];
     val t' = annotate thy algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
-    val dummy_constant = Code_Symbol.Constant @{const_name dummy_pattern};
+    val dummy_constant = Constant @{const_name dummy_pattern};
     val stmt_value =
       fold_map (translate_tyvar_sort thy algbr eqngr false) vs
       ##>> translate_typ thy algbr eqngr false ty
@@ -783,7 +785,7 @@
         val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2;
       in ((program3, ((vs_ty, t), deps)), (dep, program2)) end;
   in
-    ensure_stmt Code_Symbol.Constant stmt_value @{const_name dummy_pattern}
+    ensure_stmt Constant stmt_value @{const_name dummy_pattern}
     #> snd
     #> term_value
   end;
diff -r 626d8f08d479 -r 0940309ed8f1 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/nbe.ML	Sat Jan 25 23:50:49 2014 +0100
@@ -249,11 +249,9 @@
 
 val univs_cookie = (Univs.get, put_result, name_put);
 
-val sloppy_name = Code_Symbol.base_name;
-
 fun nbe_fun idx_of 0 (Code_Symbol.Constant "") = "nbe_value"
   | nbe_fun idx_of i sym = "c_" ^ string_of_int (idx_of sym)
-      ^ "_" ^ sloppy_name sym ^ "_" ^ string_of_int i;
+      ^ "_" ^ Code_Symbol.default_base sym ^ "_" ^ string_of_int i;
 fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n;
 fun nbe_bound v = "v_" ^ v;
 fun nbe_bound_optional NONE = "_"
@@ -266,7 +264,7 @@
 fun nbe_apps_local idx_of i c ts = nbe_fun idx_of i c `$` ml_list (rev ts);
 fun nbe_apps_constr idx_of c ts =
   let
-    val c' = if !trace then string_of_int (idx_of c) ^ " (*" ^ sloppy_name c ^ "*)"
+    val c' = if !trace then string_of_int (idx_of c) ^ " (*" ^ Code_Symbol.default_base c ^ "*)"
       else string_of_int (idx_of c);
   in name_const `$` ("(" ^ c' ^ ", " ^ ml_list (rev ts) ^ ")") end;
 
@@ -277,6 +275,7 @@
 
 end;
 
+open Basic_Code_Symbol;
 open Basic_Code_Thingol;
 
 
@@ -304,11 +303,11 @@
             else nbe_apps_constr idx_of sym ts'
       end
     and assemble_classrels classrels =
-      fold_rev (fn classrel => assemble_constapp (Code_Symbol.Class_Relation classrel) [] o single) classrels
+      fold_rev (fn classrel => assemble_constapp (Class_Relation classrel) [] o single) classrels
     and assemble_dict (Dict (classrels, x)) =
           assemble_classrels classrels (assemble_plain_dict x)
     and assemble_plain_dict (Dict_Const (inst, dss)) =
-          assemble_constapp (Code_Symbol.Class_Instance inst) dss []
+          assemble_constapp (Class_Instance inst) dss []
       | assemble_plain_dict (Dict_Var (v, (n, _))) =
           nbe_dict v n
 
@@ -429,7 +428,7 @@
       []
   | eqns_of_stmt (sym_class, Code_Thingol.Class (v, (classrels, classparams))) =
       let
-        val syms = map Code_Symbol.Class_Relation classrels @ map (Code_Symbol.Constant o fst) classparams;
+        val syms = map Class_Relation classrels @ map (Constant o fst) classparams;
         val params = Name.invent Name.context "d" (length syms);
         fun mk (k, sym) =
           (sym, ([(v, [])],
@@ -441,8 +440,8 @@
   | eqns_of_stmt (_, Code_Thingol.Classparam _) =
       []
   | eqns_of_stmt (sym_inst, Code_Thingol.Classinst { class, tyco, vs, superinsts, inst_params, ... }) =
-      [(sym_inst, (vs, [([], dummy_const (Code_Symbol.Type_Class class) [] `$$
-        map (fn (class, dss) => dummy_const (Code_Symbol.Class_Instance (tyco, class)) dss) superinsts
+      [(sym_inst, (vs, [([], dummy_const (Type_Class class) [] `$$
+        map (fn (class, dss) => dummy_const (Class_Instance (tyco, class)) dss) superinsts
         @ map (IConst o fst o snd o fst) inst_params)]))];
 
 
@@ -513,12 +512,12 @@
       | take_until f (x :: xs) = if f x then [] else x :: take_until f xs;
     fun is_dict (Const (idx, _)) =
           (case Inttab.lookup idx_tab idx of
-            SOME (Code_Symbol.Constant _) => false
+            SOME (Constant _) => false
           | _ => true)
       | is_dict (DFree _) = true
       | is_dict _ = false;
     fun const_of_idx idx =
-      case Inttab.lookup idx_tab idx of SOME (Code_Symbol.Constant const) => const;
+      case Inttab.lookup idx_tab idx of SOME (Constant const) => const;
     fun of_apps bounds (t, ts) =
       fold_map (of_univ bounds) ts
       #>> (fn ts' => list_comb (t, rev ts'))
@@ -568,7 +567,7 @@
 
 structure Nbe_Functions = Code_Data
 (
-  type T = (Univ option * int) Code_Symbol.Graph.T * (int * Code_Symbol.symbol Inttab.table);
+  type T = (Univ option * int) Code_Symbol.Graph.T * (int * Code_Symbol.T Inttab.table);
   val empty = (Code_Symbol.Graph.empty, (0, Inttab.empty));
 );