src/HOL/thy_syntax.ML
changeset 3308 da002cef7090
parent 3194 36bfceef1800
child 3345 4d888ddd6284
     1.1 --- a/src/HOL/thy_syntax.ML	Thu May 22 18:29:17 1997 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Fri May 23 09:17:26 1997 +0200
     1.3 @@ -118,9 +118,9 @@
     1.4  
     1.5    (*generate string for calling add_datatype and build_record*)
     1.6    fun mk_params ((ts, tname), cons) =
     1.7 -   ("val (thy, " ^ tname ^ "_add_primrec) = Datatype.add_datatype\n"
     1.8 +   ("val (thy," ^ tname ^ "_add_primrec," ^ tname ^ "_size_eqns) = Datatype.add_datatype\n"
     1.9      ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
    1.10 -    \val thy = thy"
    1.11 +    \val thy = ("^tname^"_add_primrec "^tname^"_size_eqns thy)"
    1.12      ,
    1.13      "structure " ^ tname ^ " =\n\
    1.14      \struct\n\
    1.15 @@ -147,7 +147,12 @@
    1.16      \val dummy = AddIffs " ^ tname ^ ".inject;\n\
    1.17      \val dummy = " ^
    1.18        (if length cons < dtK then "AddIffs " else "Addsimps ") ^
    1.19 -      tname ^ ".distinct;");
    1.20 +      tname ^ ".distinct;\n\
    1.21 +    \val dummy = Addsimps(map (fn (_,eqn) =>\n\
    1.22 +    \ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^
    1.23 +                     "] eqn (fn _ => [Simp_tac 1]))\n" ^
    1.24 +    tname^"_size_eqns)\n"
    1.25 +   );
    1.26  
    1.27    (*parsers*)
    1.28    val tvars = type_args >> map (cat "dtVar");