src/HOL/datatype.ML

     end ;
 
 in
   fun add_datatype (typevars, tname, cons_list') thy = 
     let
-      val dummy = if length cons_list' < dtK then ()
-                  else require_thy thy "Nat" "datatype definitions";
+      val dummy = require_thy thy "Arith" "datatype definitions";
       
       fun typid(dtRek(_,id)) = id
         | typid(dtVar s) = implode (tl (explode s))
         | typid(dtTyp(_,id)) = id;
 

          NoSyn);
 
       val rules_rec = rec_rules 1 cons_list
 
 (* -------------------------------------------------------------------- *)
+(* The size function                                                    *) 
+
+      fun size_eqn(_,name,types,vns,_) =
+        let fun sum((T,vn)::args) =
+                  if is_dtRek T then "size(" ^ vn ^ ") + " ^ sum(args)
+                  else sum args
+              | sum [] = "1"
+            val rhs = if exists is_dtRek types then sum(types~~vns) else "0"
+        in ("", "size(" ^ C_exp name vns ^ ") = " ^ rhs) end;
+
+      val size_eqns  = map size_eqn cons_list;
+
+(* -------------------------------------------------------------------- *)
       val consts = 
         map const_type cons_list
         @ (if num_of_cons < dtK then []
            else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)])
         @ [case_const,rec_const];

     in
       (thy |> add_types types
            |> add_arities arities
            |> add_consts consts
            |> add_trrules xrules
-           |> add_axioms rules, add_primrec)
+           |> add_axioms rules, add_primrec, size_eqns)
     end
 
 (*Check if the (induction) variable occurs among the premises, which
   usually signals a mistake *)
 fun occs_in_prems a i state =