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))