src/HOL/Tools/datatype_package.ML
changeset 17521 0f1c48de39f5
parent 17412 e26cb20ef0cc
child 17875 d81094515061
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Sep 20 15:12:40 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Sep 20 16:17:34 2005 +0200
     1.3 @@ -112,7 +112,7 @@
     1.4  
     1.5  fun constrs_of thy tname = (case datatype_info thy tname of
     1.6     SOME {index, descr, ...} =>
     1.7 -     let val (_, _, constrs) = valOf (assoc (descr, index))
     1.8 +     let val (_, _, constrs) = valOf (AList.lookup (op =) descr index)
     1.9       in SOME (map (fn (cname, _) => Const (cname, Sign.the_const_type thy cname)) constrs)
    1.10       end
    1.11   | _ => NONE);
    1.12 @@ -126,7 +126,7 @@
    1.13  fun find_tname var Bi =
    1.14    let val frees = map dest_Free (term_frees Bi)
    1.15        val params = rename_wrt_term Bi (Logic.strip_params Bi);
    1.16 -  in case assoc (frees @ params, var) of
    1.17 +  in case AList.lookup (op =) (frees @ params) var of
    1.18         NONE => error ("No such variable in subgoal: " ^ quote var)
    1.19       | SOME(Type (tn, _)) => tn
    1.20       | _ => error ("Cannot determine type of " ^ quote var)
    1.21 @@ -139,7 +139,7 @@
    1.22      val params = Logic.strip_params Bi;   (*params of subgoal i*)
    1.23      val params = rev (rename_wrt_term Bi params);   (*as they are printed*)
    1.24      val (types, sorts) = types_sorts state;
    1.25 -    fun types' (a, ~1) = (case assoc (params, a) of NONE => types(a, ~1) | sm => sm)
    1.26 +    fun types' (a, ~1) = (case AList.lookup (op =) params a of NONE => types(a, ~1) | sm => sm)
    1.27        | types' ixn = types ixn;
    1.28      val (ct, _) = read_def_cterm (sign, types', sorts) [] false (aterm, TypeInfer.logicT);
    1.29    in case #T (rep_cterm ct) of
    1.30 @@ -261,7 +261,7 @@
    1.31  
    1.32  fun dt_cases (descr: descr) (_, args, constrs) =
    1.33    let
    1.34 -    fun the_bname i = Sign.base_name (#1 (valOf (assoc (descr, i))));
    1.35 +    fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));
    1.36      val bnames = map the_bname (distinct (List.concat (map dt_recs args)));
    1.37    in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
    1.38  
    1.39 @@ -269,7 +269,7 @@
    1.40  fun induct_cases descr =
    1.41    DatatypeProp.indexify_names (List.concat (map (dt_cases descr) (map #2 descr)));
    1.42  
    1.43 -fun exhaust_cases descr i = dt_cases descr (valOf (assoc (descr, i)));
    1.44 +fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));
    1.45  
    1.46  in
    1.47  
    1.48 @@ -456,7 +456,7 @@
    1.49         strip_abs (length dts) t, is_dependent (length dts) t))
    1.50        (constrs ~~ fs);
    1.51      fun count_cases (cs, (_, _, true)) = cs
    1.52 -      | count_cases (cs, (cname, (_, body), false)) = (case assoc (cs, body) of
    1.53 +      | count_cases (cs, (cname, (_, body), false)) = (case AList.lookup (op =) cs body of
    1.54            NONE => (body, [cname]) :: cs
    1.55          | SOME cnames => AList.update (op =) (body, cnames @ [cname]) cs);
    1.56      val cases' = sort (int_ord o Library.swap o pairself (length o snd))
    1.57 @@ -489,7 +489,7 @@
    1.58  
    1.59  fun read_typ sign ((Ts, sorts), str) =
    1.60    let
    1.61 -    val T = Type.no_tvars (Sign.read_typ (sign, (curry assoc)
    1.62 +    val T = Type.no_tvars (Sign.read_typ (sign, AList.lookup (op =)
    1.63        (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
    1.64    in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
    1.65