# HG changeset patch # User wenzelm # Date 1148425495 -7200 # Node ID 9b2612b807ab63d595cf72d5dc93b48eba7c9f7b # Parent 9c84266e1d5fe1a6e21ae02161d928e248e2df18 simplified TypedefPackage.get_info; diff -r 9c84266e1d5f -r 9b2612b807ab src/HOL/Tools/typedef_codegen.ML --- a/src/HOL/Tools/typedef_codegen.ML Tue May 23 14:00:06 2006 +0200 +++ b/src/HOL/Tools/typedef_codegen.ML Wed May 24 01:04:55 2006 +0200 @@ -28,16 +28,16 @@ val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'') in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end; fun lookup f T = - (case TypedefPackage.get_typedef_info thy (get_name T) of + (case TypedefPackage.get_info thy (get_name T) of NONE => "" - | SOME (s, _) => f s); + | SOME info => f info); in (case strip_comb t of (Const (s, Type ("fun", [T, U])), ts) => - if lookup #4 T = s andalso + if lookup #Rep_name T = s andalso is_none (Codegen.get_assoc_type thy (get_name T)) then mk_fun s T ts - else if lookup #3 U = s andalso + else if lookup #Abs_name U = s andalso is_none (Codegen.get_assoc_type thy (get_name U)) then mk_fun s U ts else NONE @@ -49,9 +49,9 @@ | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps; fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) = - (case TypedefPackage.get_typedef_info thy s of + (case TypedefPackage.get_info thy s of NONE => NONE - | SOME ((newT as Type (tname, Us), oldT, Abs_name, Rep_name), _) => + | SOME {abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...} => if is_some (Codegen.get_assoc_type thy tname) then NONE else let val module' = Codegen.if_library @@ -104,8 +104,9 @@ | typedef_tycodegen thy defs gr dep module brack _ = NONE; fun typedef_type_extr thy tyco = - case TypedefPackage.get_typedef_info thy tyco - of SOME ((ty_abs, ty_rep, c_abs, c_rep), (SOME def, inject, _)) => + case TypedefPackage.get_info thy tyco + of SOME {abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, Rep_name = c_rep, + set_def = SOME def, Abs_inject = inject, ...} => let val exists_thm = UNIV_I @@ -122,8 +123,9 @@ fun typedef_fun_extr thy (c, ty) = case (fst o strip_type) ty of Type (tyco, _) :: _ => - (case TypedefPackage.get_typedef_info thy tyco - of SOME ((ty_abs, ty_rep, c_abs, c_rep), (SOME def, _, inverse)) => + (case TypedefPackage.get_info thy tyco + of SOME {abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, Rep_name = c_rep, + set_def = SOME def, Abs_inverse = inverse, ...} => if c = c_rep then let val exists_thm =