src/HOL/Tools/datatype_rep_proofs.ML
changeset 19346 c4c003abd830
parent 18728 6790126ab5f6
child 19540 d036bff01c23
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Apr 06 16:10:22 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Apr 06 16:10:46 2006 +0200
     1.3 @@ -184,7 +184,7 @@
     1.4          (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE
     1.5            (rtac exI 1 THEN
     1.6              QUIET_BREADTH_FIRST (has_fewer_prems 1)
     1.7 -            (resolve_tac rep_intrs 1))) thy |> #1)
     1.8 +            (resolve_tac rep_intrs 1))) thy |> snd)
     1.9                (parent_path flat_names thy2, types_syntax ~~ tyvars ~~
    1.10                  (Library.take (length newTs, consts)) ~~ new_type_names));
    1.11