# HG changeset patch
# User nipkow
# Date 860667655 -7200
# Node ID 602cdeabb89b6cc8e628a03f98b3315263d330bf
# Parent  4eefc6c22d414a9804991e2fc8de6a9796ac8d1a
Turned Addsimps into AddIffs for datatype laws.

diff -r 4eefc6c22d41 -r 602cdeabb89b src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Thu Apr 10 10:55:37 1997 +0200
+++ b/src/HOL/thy_syntax.ML	Thu Apr 10 12:20:55 1997 +0200
@@ -9,7 +9,7 @@
 *)
 
 (*the kind of distinctiveness axioms depends on number of constructors*)
-val dtK = 5;  (* FIXME rename?, move? *)
+val dtK = 7;  (* FIXME rename?, move? *)
 
 structure ThySynData: THY_SYN_DATA =
 struct
@@ -143,7 +143,11 @@
     \val dummy = datatypes := Dtype.build_record (thy, " ^
       mk_pair (quote tname, mk_list (map (fst o fst) cons)) ^
       ", " ^ tname ^ ".induct_tac) :: (!datatypes);\n\
-    \val dummy = Addsimps " ^ tname ^ ".simps;\n");
+    \val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\
+    \val dummy = AddIffs " ^ tname ^ ".inject;\n\
+    \val dummy = " ^
+      (if length cons < dtK then "AddIffs " else "Addsimps ") ^
+      tname ^ ".distinct;");
 
   (*parsers*)
   val tvars = type_args >> map (cat "dtVar");