src/HOL/Tools/record.ML
changeset 35742 eb8d2f668bfc
parent 35625 9c818cab0dd0
child 35989 3418cdf1855e
--- a/src/HOL/Tools/record.ML	Sat Mar 13 14:42:16 2010 +0100
+++ b/src/HOL/Tools/record.ML	Sat Mar 13 14:43:04 2010 +0100
@@ -104,8 +104,8 @@
   let
     fun get_thms thy name =
       let
-        val {Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
-          Abs_inverse = abs_inverse, ...} = Typedef.the_info thy name;
+        val [{Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
+          Abs_inverse = 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