src/HOL/Tools/record.ML
changeset 35742 eb8d2f668bfc
parent 35625 9c818cab0dd0
child 35989 3418cdf1855e
     1.1 --- a/src/HOL/Tools/record.ML	Sat Mar 13 14:42:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Mar 13 14:43:04 2010 +0100
     1.3 @@ -104,8 +104,8 @@
     1.4    let
     1.5      fun get_thms thy name =
     1.6        let
     1.7 -        val {Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
     1.8 -          Abs_inverse = abs_inverse, ...} = Typedef.the_info thy name;
     1.9 +        val [{Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
    1.10 +          Abs_inverse = abs_inverse, ...}] = Typedef.get_info_global thy name;
    1.11          val rewrite_rule =
    1.12            MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}];
    1.13        in