1.1 --- a/src/HOLCF/Tools/Domain/domain.ML	Mon Nov 08 06:58:09 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain.ML	Mon Nov 08 14:09:07 2010 -0800
     1.3 @@ -42,6 +42,11 @@
     1.4  type info =
     1.5       Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info;
     1.6  
     1.7 +fun add_arity ((b, sorts, mx), sort) thy : theory =
     1.8 +  thy
     1.9 +  |> Sign.add_types [(b, length sorts, mx)]
    1.10 +  |> AxClass.axiomatize_arity (Sign.full_name thy b, sorts, sort);
    1.11 +
    1.12  fun gen_add_domain
    1.13      (prep_sort : theory -> 'a -> sort)
    1.14      (prep_typ : theory -> (string * sort) list -> 'b -> typ)
    1.15 @@ -59,15 +64,13 @@
    1.16                  (dbind, map prep_tvar vs, mx)) raw_specs
    1.17        end;
    1.18  
    1.19 -    fun thy_type (dbind, tvars, mx) = (dbind, length tvars, mx);
    1.20      fun thy_arity (dbind, tvars, mx) =
    1.21 -      (Sign.full_name thy dbind, map (snd o dest_TFree) tvars, arg_sort false);
    1.22 +      ((dbind, map (snd o dest_TFree) tvars, mx), arg_sort false);
    1.23  
    1.24      (* this theory is used just for parsing and error checking *)
    1.25      val tmp_thy = thy
    1.26        |> Theory.copy
    1.27 -      |> Sign.add_types (map thy_type dtnvs)
    1.28 -      |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
    1.29 +      |> fold (add_arity o thy_arity) dtnvs;
    1.30  
    1.31      val dbinds : binding list =
    1.32          map (fn (_,dbind,_,_) => dbind) raw_specs;