quiet proofs;
authorwenzelm
Tue Oct 20 16:36:40 1998 +0200 (1998-10-20)
changeset 5696c2c2214f8037
parent 5695 898429dbb162
child 5697 e816c4f1a396
quiet proofs;
src/HOL/Tools/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Oct 20 16:36:21 1998 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Oct 20 16:36:40 1998 +0200
     1.3 @@ -141,13 +141,12 @@
     1.4  
     1.5      (********************************* typedef ********************************)
     1.6  
     1.7 -    (* FIXME: quiet_mode flag for TypedefPackage and BREADTH_FIRST *)
     1.8 -
     1.9      val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
    1.10 -      TypedefPackage.add_typedef_i_no_def name' (name, tvs, mx) c [] []
    1.11 -        (Some (BREADTH_FIRST (has_fewer_prems 1) (resolve_tac rep_intrs 1))) thy)
    1.12 -          (parent_path flat_names thy2, types_syntax ~~ tyvars ~~ (take (length newTs, consts)) ~~
    1.13 -            new_type_names));
    1.14 +      setmp TypedefPackage.quiet_mode true
    1.15 +        (TypedefPackage.add_typedef_i_no_def name' (name, tvs, mx) c [] []
    1.16 +          (Some (QUIET_BREADTH_FIRST (has_fewer_prems 1) (resolve_tac rep_intrs 1)))) thy)
    1.17 +            (parent_path flat_names thy2, types_syntax ~~ tyvars ~~ (take (length newTs, consts)) ~~
    1.18 +              new_type_names));
    1.19  
    1.20      (*********************** definition of constructors ***********************)
    1.21