# HG changeset patch
# User wenzelm
# Date 1003247738 -7200
# Node ID e1fd22a657ae3b0b38457f32fec76ac4a58a70c0
# Parent  b110a1ea90da54424b96e6258f1428cbd8a59316
ignore typedef result;

diff -r b110a1ea90da -r e1fd22a657ae src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Oct 16 17:55:16 2001 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Oct 16 17:55:38 2001 +0200
@@ -183,7 +183,7 @@
       setmp TypedefPackage.quiet_mode true
         (TypedefPackage.add_typedef_i_no_def name' (name, tvs, mx) c [] []
           (Some (QUIET_BREADTH_FIRST (has_fewer_prems 1)
-            (resolve_tac (Funs_nonempty::rep_intrs) 1)))) thy)
+            (resolve_tac (Funs_nonempty::rep_intrs) 1)))) thy |> #1)
               (parent_path flat_names thy2, types_syntax ~~ tyvars ~~
                 (take (length newTs, consts)) ~~ new_type_names));