1.1 --- a/src/Tools/code/code_target.ML	Sun Mar 22 11:56:22 2009 +0100
     1.2 +++ b/src/Tools/code/code_target.ML	Sun Mar 22 11:56:32 2009 +0100
     1.3 @@ -82,11 +82,9 @@
     1.4  
     1.5  (** theory data **)
     1.6  
     1.7 -structure StringPairTab = Code_Name.StringPairTab;
     1.8 -
     1.9  datatype name_syntax_table = NameSyntaxTable of {
    1.10    class: string Symtab.table,
    1.11 -  instance: unit StringPairTab.table,
    1.12 +  instance: unit Symreltab.table,
    1.13    tyco: tyco_syntax Symtab.table,
    1.14    const: const_syntax Symtab.table
    1.15  };
    1.16 @@ -99,7 +97,7 @@
    1.17      NameSyntaxTable { class = class2, instance = instance2, tyco = tyco2, const = const2 }) =
    1.18    mk_name_syntax_table (
    1.19      (Symtab.join (K snd) (class1, class2),
    1.20 -       StringPairTab.join (K snd) (instance1, instance2)),
    1.21 +       Symreltab.join (K snd) (instance1, instance2)),
    1.22      (Symtab.join (K snd) (tyco1, tyco2),
    1.23         Symtab.join (K snd) (const1, const2))
    1.24    );
    1.25 @@ -194,7 +192,7 @@
    1.26      thy
    1.27      |> (CodeTargetData.map o apfst oo Symtab.map_default)
    1.28            (target, mk_target ((serial (), seri), (([], Symtab.empty),
    1.29 -            (mk_name_syntax_table ((Symtab.empty, StringPairTab.empty), (Symtab.empty, Symtab.empty)),
    1.30 +            (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)),
    1.31                Symtab.empty))))
    1.32            ((map_target o apfst o apsnd o K) seri)
    1.33    end;
    1.34 @@ -262,11 +260,11 @@
    1.35    in if add_del then
    1.36      thy
    1.37      |> (map_name_syntax target o apfst o apsnd)
    1.38 -        (StringPairTab.update (inst, ()))
    1.39 +        (Symreltab.update (inst, ()))
    1.40    else
    1.41      thy
    1.42      |> (map_name_syntax target o apfst o apsnd)
    1.43 -        (StringPairTab.delete_safe inst)
    1.44 +        (Symreltab.delete_safe inst)
    1.45    end;
    1.46  
    1.47  fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
    1.48 @@ -407,7 +405,7 @@
    1.49        |>> map_filter I;
    1.50      val (names_class, class') = distill_names Code_Thingol.lookup_class class;
    1.51      val names_inst = map_filter (Code_Thingol.lookup_instance naming)
    1.52 -      (StringPairTab.keys instance);
    1.53 +      (Symreltab.keys instance);
    1.54      val (names_tyco, tyco') = distill_names Code_Thingol.lookup_tyco tyco;
    1.55      val (names_const, const') = distill_names Code_Thingol.lookup_const const;
    1.56      val names_hidden = names_class @ names_inst @ names_tyco @ names_const;