src/Pure/Thy/thy_parse.ML

   lexicon * (token list -> (string * string) * token list) Symtab.table;
 
 fun make_syntax keywords sects =
   let
     val dups = duplicates (map fst sects);
-    val sects' = distinct_fst_string sects;
+    val sects' = gen_distinct eq_fst sects;
   in
     if null dups then ()
     else warning ("Duplicate declaration of theory file sections:\n" ^ commas_quote dups);
     (make_lexicon (map fst sects' @ keywords), Symtab.make sects')
   end;