# HG changeset patch
# User wenzelm
# Date 908894200 -7200
# Node ID c2c2214f8037ea7d9b82e14750a53f457a616959
# Parent  898429dbb162b8bc92da87d409e17390d7ac8f19
quiet proofs;

diff -r 898429dbb162 -r c2c2214f8037 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Oct 20 16:36:21 1998 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Oct 20 16:36:40 1998 +0200
@@ -141,13 +141,12 @@
 
     (********************************* typedef ********************************)
 
-    (* FIXME: quiet_mode flag for TypedefPackage and BREADTH_FIRST *)
-
     val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
-      TypedefPackage.add_typedef_i_no_def name' (name, tvs, mx) c [] []
-        (Some (BREADTH_FIRST (has_fewer_prems 1) (resolve_tac rep_intrs 1))) thy)
-          (parent_path flat_names thy2, types_syntax ~~ tyvars ~~ (take (length newTs, consts)) ~~
-            new_type_names));
+      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 rep_intrs 1)))) thy)
+            (parent_path flat_names thy2, types_syntax ~~ tyvars ~~ (take (length newTs, consts)) ~~
+              new_type_names));
 
     (*********************** definition of constructors ***********************)