src/HOL/Tools/Quotient/quotient_typ.ML
changeset 35994 9cc3df9a606e
parent 35842 7c170d39a808
child 36323 655e2d74de3a
     1.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Sat Mar 27 18:43:11 2010 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Sat Mar 27 21:38:38 2010 +0100
     1.3 @@ -89,7 +89,7 @@
     1.4  
     1.5  
     1.6  (* tactic to prove the quot_type theorem for the new type *)
     1.7 -fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
     1.8 +fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) =
     1.9  let
    1.10    val rep_thm = #Rep typedef_info RS mem_def1
    1.11    val rep_inv = #Rep_inverse typedef_info
    1.12 @@ -143,10 +143,10 @@
    1.13    val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy
    1.14  
    1.15    (* abs and rep functions from the typedef *)
    1.16 -  val Abs_ty = #abs_type typedef_info
    1.17 -  val Rep_ty = #rep_type typedef_info
    1.18 -  val Abs_name = #Abs_name typedef_info
    1.19 -  val Rep_name = #Rep_name typedef_info
    1.20 +  val Abs_ty = #abs_type (#1 typedef_info)
    1.21 +  val Rep_ty = #rep_type (#1 typedef_info)
    1.22 +  val Abs_name = #Abs_name (#1 typedef_info)
    1.23 +  val Rep_name = #Rep_name (#1 typedef_info)
    1.24    val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
    1.25    val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
    1.26