Typedef.info: separate global and local part, only the latter is transformed by morphisms;

--- a/src/HOL/Import/proof_kernel.ML	Sat Mar 27 18:43:11 2010 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Sat Mar 27 21:38:38 2010 +0100
@@ -2098,7 +2098,7 @@
                 (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c NONE (rtac th2 1) thy
             val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
 
-            val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
+            val th3 = (#type_definition (#2 typedef_info)) RS typedef_hol2hol4
 
             val fulltyname = Sign.intern_type thy' tycname
             val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
@@ -2195,7 +2195,7 @@
                     [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)]
                     [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))]
                     typedef_hol2hollight
-            val th4 = (#type_definition typedef_info) RS typedef_hol2hollight'
+            val th4 = (#type_definition (#2 typedef_info)) RS typedef_hol2hollight'
             val _ = null (Thm.fold_terms Term.add_tvars th4 []) orelse
               raise ERR "type_introduction" "no type variables expected any more"
             val _ = null (Thm.fold_terms Term.add_vars th4 []) orelse

--- a/src/HOL/Nominal/nominal_datatype.ML	Sat Mar 27 18:43:11 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Mar 27 21:38:38 2010 +0100
@@ -640,9 +640,9 @@
             new_type_names);
 
     val perm_defs = map snd typedefs;
-    val Abs_inverse_thms = map (collect_simp o #Abs_inverse o fst) typedefs;
-    val Rep_inverse_thms = map (#Rep_inverse o fst) typedefs;
-    val Rep_thms = map (collect_simp o #Rep o fst) typedefs;
+    val Abs_inverse_thms = map (collect_simp o #Abs_inverse o snd o fst) typedefs;
+    val Rep_inverse_thms = map (#Rep_inverse o snd o fst) typedefs;
+    val Rep_thms = map (collect_simp o #Rep o snd o fst) typedefs;
 
 
     (** prove that new types are in class pt_<name> **)
@@ -826,8 +826,8 @@
         new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax)
       (thy7, [], [], []);
 
-    val abs_inject_thms = map (collect_simp o #Abs_inject o fst) typedefs
-    val rep_inject_thms = map (#Rep_inject o fst) typedefs
+    val abs_inject_thms = map (collect_simp o #Abs_inject o snd o fst) typedefs
+    val rep_inject_thms = map (#Rep_inject o snd o fst) typedefs
 
     (* prove theorem  Rep_i (Constr_j ...) = Constr'_j ...  *)
 

--- a/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 27 18:43:11 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 27 21:38:38 2010 +0100
@@ -276,11 +276,11 @@
 
     val _ = message config "Proving isomorphism properties ...";
 
-    val newT_iso_axms = map (fn (_, td) =>
+    val newT_iso_axms = map (fn (_, (_, td)) =>
       (collect_simp (#Abs_inverse td), #Rep_inverse td,
        collect_simp (#Rep td))) typedefs;
 
-    val newT_iso_inj_thms = map (fn (_, td) =>
+    val newT_iso_inj_thms = map (fn (_, (_, td)) =>
       (collect_simp (#Abs_inject td) RS iffD1, #Rep_inject td RS iffD1)) typedefs;
 
     (********* isomorphisms between existing types and "unfolded" types *******)

--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Mar 27 18:43:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Mar 27 21:38:38 2010 +0100
@@ -570,8 +570,8 @@
           set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
   else case Typedef.get_info_global thy s of
     (* FIXME handle multiple typedef interpretations (!??) *)
-    [{abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
-          Rep_inverse, ...}] =>
+    [({abs_type, rep_type, Abs_name, Rep_name, ...}, {set_def, Rep, Abs_inverse,
+          Rep_inverse, ...})] =>
     SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
           Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
           set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,

--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Sat Mar 27 18:43:11 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Sat Mar 27 21:38:38 2010 +0100
@@ -89,7 +89,7 @@
 
 
 (* tactic to prove the quot_type theorem for the new type *)
-fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
+fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) =
 let
   val rep_thm = #Rep typedef_info RS mem_def1
   val rep_inv = #Rep_inverse typedef_info
@@ -143,10 +143,10 @@
   val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy
 
   (* abs and rep functions from the typedef *)
-  val Abs_ty = #abs_type typedef_info
-  val Rep_ty = #rep_type typedef_info
-  val Abs_name = #Abs_name typedef_info
-  val Rep_name = #Rep_name typedef_info
+  val Abs_ty = #abs_type (#1 typedef_info)
+  val Rep_ty = #rep_type (#1 typedef_info)
+  val Abs_name = #Abs_name (#1 typedef_info)
+  val Rep_name = #Rep_name (#1 typedef_info)
   val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
   val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
 

--- a/src/HOL/Tools/record.ML	Sat Mar 27 18:43:11 2010 +0100
+++ b/src/HOL/Tools/record.ML	Sat Mar 27 21:38:38 2010 +0100
@@ -104,12 +104,12 @@
   let
     fun get_thms thy name =
       let
-        val [{Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
-          Abs_inverse = abs_inverse, ...}] = Typedef.get_info_global thy name;
+        val [({Abs_name, abs_type = absT, ...}, {Rep_inject, Abs_inverse, ...})] =
+          Typedef.get_info_global thy name;
         val rewrite_rule =
           MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}];
       in
-        (map rewrite_rule [rep_inject, abs_inverse], Const (absN, repT --> absT), absT)
+        (map rewrite_rule [Rep_inject, Abs_inverse], Const (Abs_name, repT --> absT), absT)
       end;
   in
     thy

--- a/src/HOL/Tools/typecopy.ML	Sat Mar 27 18:43:11 2010 +0100
+++ b/src/HOL/Tools/typecopy.ML	Sat Mar 27 21:38:38 2010 +0100
@@ -55,9 +55,9 @@
     val vs =
       AList.make (the_default HOLogic.typeS o AList.lookup (op =) (Term.add_tfreesT ty [])) raw_vs;
     val tac = Tactic.rtac UNIV_witness 1;
-    fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
-      Rep_name = c_rep, Abs_inject = inject,
-      Abs_inverse = inverse, ... } : Typedef.info ) thy =
+    fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
+          Rep_name = c_rep, ...}, { Abs_inject = inject, Abs_inverse = inverse, ... })
+          : Typedef.info) thy =
         let
           val exists_thm =
             UNIV_I
@@ -94,7 +94,7 @@
     val SOME { constr = c, proj = (proj, _), proj_def = proj_eq, vs = vs,
       typ = ty_rep, ... } = get_info thy tyco;
     (* FIXME handle multiple typedef interpretations (!??) *)
-    val [{ Rep_inject = proj_inject, ... }] = Typedef.get_info_global thy tyco;
+    val [(_, { Rep_inject = proj_inject, ... })] = Typedef.get_info_global thy tyco;
     val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c));
     val ty = Type (tyco, map TFree vs);
     val proj = Const (proj, ty --> ty_rep);

--- a/src/HOL/Tools/typedef.ML	Sat Mar 27 18:43:11 2010 +0100
+++ b/src/HOL/Tools/typedef.ML	Sat Mar 27 21:38:38 2010 +0100
@@ -8,8 +8,8 @@
 signature TYPEDEF =
 sig
   type info =
-   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm,
-    type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
+   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string} *
+   {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
     Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
     Rep_induct: thm, Abs_induct: thm}
   val transform_info: morphism -> info -> info
@@ -35,26 +35,26 @@
 (* theory data *)
 
 type info =
- {(*global part*)
-  rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
+  (*global part*)
+  {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string} *
   (*local part*)
-  inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
-  Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
-  Rep_induct: thm, Abs_induct: thm};
+  {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
+    Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
+    Rep_induct: thm, Abs_induct: thm};
 
 fun transform_info phi (info: info) =
   let
     val thm = Morphism.thm phi;
-    val {rep_type, abs_type, Rep_name, Abs_name, inhabited, type_definition,
+    val (global_info, {inhabited, type_definition,
       set_def, Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
-      Rep_cases, Abs_cases, Rep_induct, Abs_induct} = info;
+      Rep_cases, Abs_cases, Rep_induct, Abs_induct}) = info;
   in
-   {rep_type = rep_type, abs_type = abs_type, Rep_name = Rep_name, Abs_name = Abs_name,
-    inhabited = thm inhabited, type_definition = thm type_definition,
-    set_def = Option.map thm set_def, Rep = thm Rep, Rep_inverse = thm Rep_inverse,
-    Abs_inverse = thm Abs_inverse, Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject,
-    Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases, Rep_induct = thm Rep_induct,
-    Abs_induct = thm Abs_induct}
+    (global_info,
+     {inhabited = thm inhabited, type_definition = thm type_definition,
+      set_def = Option.map thm set_def, Rep = thm Rep, Rep_inverse = thm Rep_inverse,
+      Abs_inverse = thm Abs_inverse, Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject,
+      Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases, Rep_induct = thm Rep_induct,
+      Abs_induct = thm Abs_induct})
   end;
 
 structure Data = Generic_Data
@@ -235,12 +235,13 @@
                 [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname]),
               make @{thm type_definition.Abs_induct});
 
-        val info = {rep_type = oldT, abs_type = newT,
-          Rep_name = #1 (Term.dest_Const RepC), Abs_name = #1 (Term.dest_Const AbsC),
-            inhabited = inhabited, type_definition = type_definition, set_def = set_def,
+        val info =
+          ({rep_type = oldT, abs_type = newT,
+            Rep_name = #1 (Term.dest_Const RepC), Abs_name = #1 (Term.dest_Const AbsC)},
+           {inhabited = inhabited, type_definition = type_definition, set_def = set_def,
             Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
             Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
-          Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct};
+          Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct});
       in
         lthy2
         |> Local_Theory.declaration true (fn phi => put_info full_tname (transform_info phi info))

--- a/src/HOL/Tools/typedef_codegen.ML	Sat Mar 27 18:43:11 2010 +0100
+++ b/src/HOL/Tools/typedef_codegen.ML	Sat Mar 27 21:38:38 2010 +0100
@@ -31,10 +31,10 @@
   in
     (case strip_comb t of
        (Const (s, Type ("fun", [T, U])), ts) =>
-         if lookup #Rep_name T = s andalso
+         if lookup (#Rep_name o #1) T = s andalso
            is_none (Codegen.get_assoc_type thy (get_name T))
          then mk_fun s T ts
-         else if lookup #Abs_name U = s andalso
+         else if lookup (#Abs_name o #1) U = s andalso
            is_none (Codegen.get_assoc_type thy (get_name U))
          then mk_fun s U ts
          else NONE
@@ -48,7 +48,7 @@
 fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
       (case Typedef.get_info_global thy s of
         (* FIXME handle multiple typedef interpretations (!??) *)
-        [{abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...}] =>
+        [({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

--- a/src/HOLCF/Tools/pcpodef.ML	Sat Mar 27 18:43:11 2010 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML	Sat Mar 27 21:38:38 2010 +0100
@@ -193,10 +193,10 @@
 fun add_podef def opt_name typ set opt_morphs tac thy =
   let
     val name = the_default (#1 typ) opt_name;
-    val ((full_tname, info as {type_definition, set_def, Rep_name, ...}), thy2) = thy
+    val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy2) = thy
       |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac;
-    val oldT = #rep_type info;
-    val newT = #abs_type info;
+    val oldT = #rep_type (#1 info);
+    val newT = #abs_type (#1 info);
     val lhs_tfrees = map dest_TFree (snd (dest_Type newT));
 
     val RepC = Const (Rep_name, newT --> oldT);
@@ -235,7 +235,7 @@
 
     fun cpodef_result nonempty admissible thy =
       let
-        val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy
+        val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
           |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1);
         val (cpo_info, thy3) = thy2
           |> prove_cpo name newT morphs type_definition set_def below_def admissible;
@@ -270,7 +270,7 @@
     fun pcpodef_result UU_mem admissible thy =
       let
         val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1;
-        val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy
+        val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
           |> add_podef def (SOME name) typ set opt_morphs tac;
         val (cpo_info, thy3) = thy2
           |> prove_cpo name newT morphs type_definition set_def below_def admissible;

--- a/src/HOLCF/Tools/repdef.ML	Sat Mar 27 18:43:11 2010 +0100
+++ b/src/HOLCF/Tools/repdef.ML	Sat Mar 27 21:38:38 2010 +0100
@@ -95,8 +95,8 @@
       |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2);
 
     (*definitions*)
-    val Rep_const = Const (#Rep_name info, newT --> udomT);
-    val Abs_const = Const (#Abs_name info, udomT --> newT);
+    val Rep_const = Const (#Rep_name (#1 info), newT --> udomT);
+    val Abs_const = Const (#Abs_name (#1 info), udomT --> newT);
     val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const);
     val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $
       Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0)));
@@ -125,8 +125,8 @@
     val approx_def = singleton (ProofContext.export lthy ctxt_thy) approx_ldef;
     val type_definition_thm =
       MetaSimplifier.rewrite_rule
-        (the_list (#set_def info))
-        (#type_definition info);
+        (the_list (#set_def (#2 info)))
+        (#type_definition (#2 info));
     val typedef_thms =
       [type_definition_thm, #below_def cpo_info, emb_def, prj_def, approx_def];
     val thy = lthy