src/HOL/Tools/typecopy.ML
changeset 35994 9cc3df9a606e
parent 35845 e5980f0ad025
child 36150 123f721c9a37
     1.1 --- a/src/HOL/Tools/typecopy.ML	Sat Mar 27 18:43:11 2010 +0100
     1.2 +++ b/src/HOL/Tools/typecopy.ML	Sat Mar 27 21:38:38 2010 +0100
     1.3 @@ -55,9 +55,9 @@
     1.4      val vs =
     1.5        AList.make (the_default HOLogic.typeS o AList.lookup (op =) (Term.add_tfreesT ty [])) raw_vs;
     1.6      val tac = Tactic.rtac UNIV_witness 1;
     1.7 -    fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
     1.8 -      Rep_name = c_rep, Abs_inject = inject,
     1.9 -      Abs_inverse = inverse, ... } : Typedef.info ) thy =
    1.10 +    fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
    1.11 +          Rep_name = c_rep, ...}, { Abs_inject = inject, Abs_inverse = inverse, ... })
    1.12 +          : Typedef.info) thy =
    1.13          let
    1.14            val exists_thm =
    1.15              UNIV_I
    1.16 @@ -94,7 +94,7 @@
    1.17      val SOME { constr = c, proj = (proj, _), proj_def = proj_eq, vs = vs,
    1.18        typ = ty_rep, ... } = get_info thy tyco;
    1.19      (* FIXME handle multiple typedef interpretations (!??) *)
    1.20 -    val [{ Rep_inject = proj_inject, ... }] = Typedef.get_info_global thy tyco;
    1.21 +    val [(_, { Rep_inject = proj_inject, ... })] = Typedef.get_info_global thy tyco;
    1.22      val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c));
    1.23      val ty = Type (tyco, map TFree vs);
    1.24      val proj = Const (proj, ty --> ty_rep);