# 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 =