tuned: distinct_fst_string;
authorwenzelm
Mon Nov 03 17:55:55 1997 +0100 (1997-11-03)
changeset 4101e8ad51c88be9
parent 4100 9f6907c40442
child 4102 f746af27164b
tuned: distinct_fst_string;
src/Pure/Syntax/syntax.ML
src/Pure/Thy/thy_parse.ML
src/Pure/name_space.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Mon Nov 03 14:37:35 1997 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Nov 03 17:55:55 1997 +0100
     1.3 @@ -96,7 +96,7 @@
     1.4  (** tables of token translation functions **)
     1.5  
     1.6  fun lookup_tokentr tabs modes =
     1.7 -  let val trs = gen_distinct eq_fst (flat (map (assocs tabs) (modes @ [""])))
     1.8 +  let val trs = distinct_fst_string (flat (map (assocs tabs) (modes @ [""])))
     1.9    in fn c => apsome fst (assoc (trs, c)) end;
    1.10  
    1.11  fun merge_tokentrtabs tabs1 tabs2 =
     2.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Nov 03 14:37:35 1997 +0100
     2.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Nov 03 17:55:55 1997 +0100
     2.3 @@ -440,7 +440,7 @@
     2.4  fun make_syntax keywords sects =
     2.5    let
     2.6      val dups = duplicates (map fst sects);
     2.7 -    val sects' = gen_distinct eq_fst sects;
     2.8 +    val sects' = distinct_fst_string sects;
     2.9    in
    2.10      if null dups then ()
    2.11      else warning ("Duplicate declaration of theory file sections:\n" ^ commas_quote dups);
     3.1 --- a/src/Pure/name_space.ML	Mon Nov 03 14:37:35 1997 +0100
     3.2 +++ b/src/Pure/name_space.ML	Mon Nov 03 17:55:55 1997 +0100
     3.3 @@ -72,8 +72,7 @@
     3.4            in
     3.5              map (rpair p o pack) (sfxs @ pfxs)
     3.6            end;
     3.7 -    val mapping = filter_out (op =)
     3.8 -      (gen_distinct eq_fst (flat (map accesses entries)));
     3.9 +    val mapping = filter_out (op =) (distinct_fst_string (flat (map accesses entries)));
    3.10    in
    3.11      NameSpace (entries, Symtab.make mapping)
    3.12    end;