# HG changeset patch
# User haftmann
# Date 1144332577 -7200
# Node ID 91c348f05f1ac9679889ecd8ffd9c1e25e9a6d22
# Parent  094a1c071c8eb7988abbb9ba973517fe2fe0c11d
adaptions to change in typedef_package.ML

diff -r 094a1c071c8e -r 91c348f05f1a src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Thu Apr 06 16:09:20 2006 +0200
+++ b/src/HOL/Tools/record_package.ML	Thu Apr 06 16:09:37 2006 +0200
@@ -1281,9 +1281,10 @@
   let
     val UNIV = HOLogic.mk_UNIV repT;
 
-    val (thy',{set_def=SOME def, Abs_induct = abs_induct,
-               Abs_inject=abs_inject, Abs_inverse = abs_inverse,...}) =
-        thy |> setmp TypedefPackage.quiet_mode true
+    val ({set_def=SOME def, Abs_induct = abs_induct,
+               Abs_inject=abs_inject, Abs_inverse = abs_inverse,...}, thy') =
+        thy
+        |> setmp TypedefPackage.quiet_mode true
            (TypedefPackage.add_typedef_i true NONE
              (suffix ext_typeN (Sign.base_name name), alphas, Syntax.NoSyn) UNIV NONE
              (Tactic.rtac UNIV_witness 1))