src/HOL/Tools/datatype_rep_proofs.ML
changeset 11822 122834177ec1
parent 11806 e1fd22a657ae
child 11827 16ef206e6648
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Oct 17 20:24:37 2001 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Oct 17 20:25:19 2001 +0200
     1.3 @@ -181,9 +181,9 @@
     1.4  
     1.5      val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
     1.6        setmp TypedefPackage.quiet_mode true
     1.7 -        (TypedefPackage.add_typedef_i_no_def name' (name, tvs, mx) c [] []
     1.8 -          (Some (QUIET_BREADTH_FIRST (has_fewer_prems 1)
     1.9 -            (resolve_tac (Funs_nonempty::rep_intrs) 1)))) thy |> #1)
    1.10 +        (TypedefPackage.add_typedef_i false name' (name, tvs, mx) c None
    1.11 +          (QUIET_BREADTH_FIRST (has_fewer_prems 1)
    1.12 +            (resolve_tac (Funs_nonempty::rep_intrs) 1))) thy |> #1)
    1.13                (parent_path flat_names thy2, types_syntax ~~ tyvars ~~
    1.14                  (take (length newTs, consts)) ~~ new_type_names));
    1.15