src/Tools/Code/code_target.ML

 fun the_reserved (Target { reserved, ... }) = reserved;
 fun the_includes (Target { includes, ... }) = includes;
 fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
 fun the_module_alias (Target { module_alias , ... }) = module_alias;
 
-structure CodeTargetData = Theory_Data
+structure Targets = Theory_Data
 (
   type T = (target Symtab.table * string list) * int;
   val empty = ((Symtab.empty, []), 80);
   val extend = I;
   fun merge (((target1, exc1), width1), ((target2, exc2), width2)) : T =
     ((Symtab.join (merge_target true) (target1, target2),
       Library.merge (op =) (exc1, exc2)), Int.max (width1, width2));
 );
 
-val abort_allowed = snd o fst o CodeTargetData.get;
-
-val the_default_width = snd o CodeTargetData.get;
-
-fun assert_target thy target = if Symtab.defined ((fst o fst) (CodeTargetData.get thy)) target
+val abort_allowed = snd o fst o Targets.get;
+
+val the_default_width = snd o Targets.get;
+
+fun assert_target thy target = if Symtab.defined ((fst o fst) (Targets.get thy)) target
   then target
   else error ("Unknown code target language: " ^ quote target);
 
 fun put_target (target, seri) thy =
   let
-    val lookup_target = Symtab.lookup ((fst o fst) (CodeTargetData.get thy));
+    val lookup_target = Symtab.lookup ((fst o fst) (Targets.get thy));
     val _ = case seri
      of Extends (super, _) => if is_some (lookup_target super) then ()
           else error ("Unknown code target language: " ^ quote super)
       | _ => ();
     val overwriting = case (Option.map the_serializer o lookup_target) target

     val _ = if overwriting
       then warning ("Overwriting existing target " ^ quote target)
       else (); 
   in
     thy
-    |> (CodeTargetData.map o apfst o apfst oo Symtab.map_default)
+    |> (Targets.map o apfst o apfst o Symtab.update)
           (target, make_target ((serial (), seri), (([], Symtab.empty),
             (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)),
               Symtab.empty))))
-          ((map_target o apfst o apsnd o K) seri)
   end;
 
 fun add_target (target, seri) = put_target (target, Serializer seri);
 fun extend_target (target, (super, modify)) =
   put_target (target, Extends (super, modify));

 fun map_target_data target f thy =
   let
     val _ = assert_target thy target;
   in
     thy
-    |> (CodeTargetData.map o apfst o apfst o Symtab.map_entry target o map_target) f
+    |> (Targets.map o apfst o apfst o Symtab.map_entry target o map_target) f
   end;
 
 fun map_reserved target =
   map_target_data target o apsnd o apfst o apfst;
 fun map_includes target =

 fun map_name_syntax target =
   map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table;
 fun map_module_alias target =
   map_target_data target o apsnd o apsnd o apsnd;
 
-fun set_default_code_width k = (CodeTargetData.map o apsnd) (K k);
+fun set_default_code_width k = (Targets.map o apsnd) (K k);
 
 
 (** serializer usage **)
 
 (* montage *)
 
 fun the_literals thy =
   let
-    val ((targets, _), _) = CodeTargetData.get thy;
+    val ((targets, _), _) = Targets.get thy;
     fun literals target = case Symtab.lookup targets target
      of SOME data => (case the_serializer data
          of Serializer (_, literals) => literals
           | Extends (super, _) => literals super)
       | NONE => error ("Unknown code target language: " ^ quote target);

       program4 names2
   end;
 
 fun mount_serializer thy alt_serializer target some_width module args naming program names =
   let
-    val ((targets, abortable), default_width) = CodeTargetData.get thy;
+    val ((targets, abortable), default_width) = Targets.get thy;
     fun collapse_hierarchy target =
       let
         val data = case Symtab.lookup targets target
          of SOME data => data
           | NONE => error ("Unknown code target language: " ^ quote target);

   end;
 
 fun gen_allow_abort prep_const raw_c thy =
   let
     val c = prep_const thy raw_c;
-  in thy |> (CodeTargetData.map o apfst o apsnd) (insert (op =) c) end;
+  in thy |> (Targets.map o apfst o apsnd) (insert (op =) c) end;
 
 
 (* concrete syntax *)
 
 local