src/HOL/Tools/datatype_rep_proofs.ML
changeset 9315 f793f05024f6
parent 8479 5d327a46dc61
child 10911 eb5721204b38
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Jul 13 23:11:38 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Jul 13 23:13:10 2000 +0200
     1.3 @@ -233,7 +233,7 @@
     1.4            (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
     1.5          val (thy', [def_thm]) = thy |>
     1.6            Theory.add_consts_i [(cname', constrT, mx)] |>
     1.7 -          (PureThy.add_defs_i o map Thm.no_attributes) [(def_name, def)];
     1.8 +          (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)];
     1.9  
    1.10        in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
    1.11  
    1.12 @@ -381,7 +381,7 @@
    1.13          val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
    1.14            equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $
    1.15              list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos);
    1.16 -        val (thy', def_thms) = (PureThy.add_defs_i o map Thm.no_attributes) defs thy;
    1.17 +        val (thy', def_thms) = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy;
    1.18  
    1.19          (* prove characteristic equations *)
    1.20