src/Tools/code/code_target.ML

   | mk_serialization target _ _ string code (String _) = SOME (string code);
 
 
 (** theory data **)
 
-structure StringPairTab = Code_Name.StringPairTab;
-
 datatype name_syntax_table = NameSyntaxTable of {
   class: string Symtab.table,
-  instance: unit StringPairTab.table,
+  instance: unit Symreltab.table,
   tyco: tyco_syntax Symtab.table,
   const: const_syntax Symtab.table
 };
 
 fun mk_name_syntax_table ((class, instance), (tyco, const)) =

   mk_name_syntax_table (f ((class, instance), (tyco, const)));
 fun merge_name_syntax_table (NameSyntaxTable { class = class1, instance = instance1, tyco = tyco1, const = const1 },
     NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
   mk_name_syntax_table (
     (Symtab.join (K snd) (class1, class2),
-       StringPairTab.join (K snd) (instance1, instance2)),
+       Symreltab.join (K snd) (instance1, instance2)),
     (Symtab.join (K snd) (tyco1, tyco2),
        Symtab.join (K snd) (const1, const2))
   );
 
 type serializer =

       else (); 
   in
     thy
     |> (CodeTargetData.map o apfst oo Symtab.map_default)
           (target, mk_target ((serial (), seri), (([], Symtab.empty),
-            (mk_name_syntax_table ((Symtab.empty, StringPairTab.empty), (Symtab.empty, 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);

   let
     val inst = (prep_class thy raw_class, prep_tyco thy raw_tyco);
   in if add_del then
     thy
     |> (map_name_syntax target o apfst o apsnd)
-        (StringPairTab.update (inst, ()))
+        (Symreltab.update (inst, ()))
   else
     thy
     |> (map_name_syntax target o apfst o apsnd)
-        (StringPairTab.delete_safe inst)
+        (Symreltab.delete_safe inst)
   end;
 
 fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
   let
     val tyco = prep_tyco thy raw_tyco;

            of SOME name => (SOME name, Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
             | NONE => (NONE, tab)) (Symtab.keys src_tab)
       |>> map_filter I;
     val (names_class, class') = distill_names Code_Thingol.lookup_class class;
     val names_inst = map_filter (Code_Thingol.lookup_instance naming)
-      (StringPairTab.keys instance);
+      (Symreltab.keys instance);
     val (names_tyco, tyco') = distill_names Code_Thingol.lookup_tyco tyco;
     val (names_const, const') = distill_names Code_Thingol.lookup_const const;
     val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
     val names2 = subtract (op =) names_hidden names1;
     val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;