src/HOL/Tools/datatype_codegen.ML
changeset 17521 0f1c48de39f5
parent 17412 e26cb20ef0cc
child 18220 43cf5767f992
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Sep 20 15:12:40 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Sep 20 16:17:34 2005 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5  fun find_nonempty (descr: DatatypeAux.descr) is i =
     1.6    let
     1.7 -    val (_, _, constrs) = valOf (assoc (descr, i));
     1.8 +    val (_, _, constrs) = valOf (AList.lookup (op =) descr i);
     1.9      fun arg_nonempty (_, DatatypeAux.DtRec i) = if i mem is then NONE
    1.10            else Option.map (curry op + 1 o snd) (find_nonempty descr (i::is) i)
    1.11        | arg_nonempty _ = SOME 0;
    1.12 @@ -160,7 +160,7 @@
    1.13                   [Pretty.block [Pretty.str "(case", Pretty.brk 1,
    1.14                     Pretty.str "i", Pretty.brk 1, Pretty.str "of",
    1.15                     Pretty.brk 1, Pretty.str "0 =>", Pretty.brk 1,
    1.16 -                   mk_constr "0" true (cname, valOf (assoc (cs, cname))),
    1.17 +                   mk_constr "0" true (cname, valOf (AList.lookup (op =) cs cname)),
    1.18                     Pretty.brk 1, Pretty.str "| _ =>", Pretty.brk 1,
    1.19                     mk_choice cs1, Pretty.str ")"]]
    1.20                 else [mk_choice cs2])) ::
    1.21 @@ -263,15 +263,15 @@
    1.22     (c as Const (s, T), ts) =>
    1.23         (case find_first (fn (_, {index, descr, case_name, ...}) =>
    1.24           s = case_name orelse
    1.25 -           isSome (assoc (#3 (valOf (assoc (descr, index))), s)))
    1.26 +           AList.defined (op =) ((#3 o the o AList.lookup (op =) descr) index) s)
    1.27               (Symtab.dest (DatatypePackage.get_datatypes thy)) of
    1.28            NONE => NONE
    1.29          | SOME (tname, {index, descr, ...}) =>
    1.30             if isSome (get_assoc_code thy s T) then NONE else
    1.31 -           let val SOME (_, _, constrs) = assoc (descr, index)
    1.32 -           in (case (assoc (constrs, s), strip_type T) of
    1.33 +           let val SOME (_, _, constrs) = AList.lookup (op =) descr index
    1.34 +           in (case (AList.lookup (op =) constrs s, strip_type T) of
    1.35                 (NONE, _) => SOME (pretty_case thy defs gr dep module brack
    1.36 -                 (#3 (valOf (assoc (descr, index)))) c ts)
    1.37 +                 (#3 (valOf (AList.lookup (op =) descr index))) c ts)
    1.38               | (SOME args, (_, Type _)) => SOME (pretty_constr thy defs
    1.39                   (fst (invoke_tycodegen thy defs dep module false
    1.40                      (gr, snd (strip_type T))))