src/HOL/thy_syntax.ML
changeset 2930 602cdeabb89b
parent 2922 580647a879cf
child 3194 36bfceef1800
     1.1 --- a/src/HOL/thy_syntax.ML	Thu Apr 10 10:55:37 1997 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Thu Apr 10 12:20:55 1997 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  *)
     1.5  
     1.6  (*the kind of distinctiveness axioms depends on number of constructors*)
     1.7 -val dtK = 5;  (* FIXME rename?, move? *)
     1.8 +val dtK = 7;  (* FIXME rename?, move? *)
     1.9  
    1.10  structure ThySynData: THY_SYN_DATA =
    1.11  struct
    1.12 @@ -143,7 +143,11 @@
    1.13      \val dummy = datatypes := Dtype.build_record (thy, " ^
    1.14        mk_pair (quote tname, mk_list (map (fst o fst) cons)) ^
    1.15        ", " ^ tname ^ ".induct_tac) :: (!datatypes);\n\
    1.16 -    \val dummy = Addsimps " ^ tname ^ ".simps;\n");
    1.17 +    \val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\
    1.18 +    \val dummy = AddIffs " ^ tname ^ ".inject;\n\
    1.19 +    \val dummy = " ^
    1.20 +      (if length cons < dtK then "AddIffs " else "Addsimps ") ^
    1.21 +      tname ^ ".distinct;");
    1.22  
    1.23    (*parsers*)
    1.24    val tvars = type_args >> map (cat "dtVar");