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