src/HOL/Tools/typedef_codegen.ML
changeset 35994 9cc3df9a606e
parent 35743 c506c029a082
child 36692 54b64d4ad524
     1.1 --- a/src/HOL/Tools/typedef_codegen.ML	Sat Mar 27 18:43:11 2010 +0100
     1.2 +++ b/src/HOL/Tools/typedef_codegen.ML	Sat Mar 27 21:38:38 2010 +0100
     1.3 @@ -31,10 +31,10 @@
     1.4    in
     1.5      (case strip_comb t of
     1.6         (Const (s, Type ("fun", [T, U])), ts) =>
     1.7 -         if lookup #Rep_name T = s andalso
     1.8 +         if lookup (#Rep_name o #1) T = s andalso
     1.9             is_none (Codegen.get_assoc_type thy (get_name T))
    1.10           then mk_fun s T ts
    1.11 -         else if lookup #Abs_name U = s andalso
    1.12 +         else if lookup (#Abs_name o #1) U = s andalso
    1.13             is_none (Codegen.get_assoc_type thy (get_name U))
    1.14           then mk_fun s U ts
    1.15           else NONE
    1.16 @@ -48,7 +48,7 @@
    1.17  fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
    1.18        (case Typedef.get_info_global thy s of
    1.19          (* FIXME handle multiple typedef interpretations (!??) *)
    1.20 -        [{abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...}] =>
    1.21 +        [({abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...}, _)] =>
    1.22            if is_some (Codegen.get_assoc_type thy tname) then NONE
    1.23            else
    1.24              let