1.1 --- a/src/HOL/Tools/record_package.ML	Thu Apr 06 16:09:20 2006 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Thu Apr 06 16:09:37 2006 +0200
     1.3 @@ -1281,9 +1281,10 @@
     1.4    let
     1.5      val UNIV = HOLogic.mk_UNIV repT;
     1.6  
     1.7 -    val (thy',{set_def=SOME def, Abs_induct = abs_induct,
     1.8 -               Abs_inject=abs_inject, Abs_inverse = abs_inverse,...}) =
     1.9 -        thy |> setmp TypedefPackage.quiet_mode true
    1.10 +    val ({set_def=SOME def, Abs_induct = abs_induct,
    1.11 +               Abs_inject=abs_inject, Abs_inverse = abs_inverse,...}, thy') =
    1.12 +        thy
    1.13 +        |> setmp TypedefPackage.quiet_mode true
    1.14             (TypedefPackage.add_typedef_i true NONE
    1.15               (suffix ext_typeN (Sign.base_name name), alphas, Syntax.NoSyn) UNIV NONE
    1.16               (Tactic.rtac UNIV_witness 1))