src/Pure/Thy/thy_parse.ML
changeset 17496 26535df536ae
parent 17412 e26cb20ef0cc
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Tue Sep 20 08:20:22 2005 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue Sep 20 08:21:49 2005 +0200
     1.3 @@ -284,8 +284,8 @@
     1.4        [(parens (commas [t, mk_list xs, rhs, syn]), true)];
     1.5  
     1.6  fun mk_type_decls tys =
     1.7 -  "|> Theory.add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
     1.8 -  \|> Theory.add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
     1.9 +  "|> Theory.add_types\n" ^ mk_big_list (AList.find (op =) tys false) ^ "\n\n\
    1.10 +  \|> Theory.add_tyabbrs\n" ^ mk_big_list (AList.find (op =) tys true);
    1.11  
    1.12  
    1.13  val old_type_decl = names1 -- nat -- opt_infix >> mk_old_type_decl;
    1.14 @@ -390,8 +390,8 @@
    1.15  (* instance *)
    1.16  
    1.17  fun mk_witness (axths, opt_tac) =
    1.18 -  mk_list (keyfilter axths false) ^ "\n" ^
    1.19 -  mk_list (keyfilter axths true) ^ "\n" ^
    1.20 +  mk_list (AList.find (op =) axths false) ^ "\n" ^
    1.21 +  mk_list (AList.find (op =) axths true) ^ "\n" ^
    1.22    opt_tac;
    1.23  
    1.24  val axm_or_thm =
    1.25 @@ -441,7 +441,7 @@
    1.26  fun make_syntax keywords sects =
    1.27    let
    1.28      val dups = duplicates (map fst sects);
    1.29 -    val sects' = gen_distinct eq_fst sects;
    1.30 +    val sects' = gen_distinct (eq_fst (op =)) sects;
    1.31      val keys = map Symbol.explode (map fst sects' @ keywords);
    1.32    in
    1.33      if null dups then ()