src/Pure/Thy/thy_parse.ML
changeset 4101 e8ad51c88be9
parent 4099 0ec0d2dbe3f4
child 4103 884968ad30da
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Nov 03 14:37:35 1997 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Nov 03 17:55:55 1997 +0100
     1.3 @@ -440,7 +440,7 @@
     1.4  fun make_syntax keywords sects =
     1.5    let
     1.6      val dups = duplicates (map fst sects);
     1.7 -    val sects' = gen_distinct eq_fst sects;
     1.8 +    val sects' = distinct_fst_string sects;
     1.9    in
    1.10      if null dups then ()
    1.11      else warning ("Duplicate declaration of theory file sections:\n" ^ commas_quote dups);