for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML

--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Apr 12 13:19:28 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Apr 12 15:05:42 2010 -0700
@@ -15,7 +15,7 @@
       binding * term -> theory -> thm * theory
 
   val add_axioms :
-      (binding * (typ * typ)) list -> theory ->
+      (binding * mixfix * (typ * typ)) list -> theory ->
       (Domain_Take_Proofs.iso_info list
        * Domain_Take_Proofs.take_induct_info) * theory
 end;
@@ -89,33 +89,47 @@
   end;
 
 fun add_axioms
-    (dom_eqns : (binding * (typ * typ)) list)
+    (dom_eqns : (binding * mixfix * (typ * typ)) list)
     (thy : theory) =
   let
 
+    val dbinds = map #1 dom_eqns;
+
+    (* declare new types *)
+    fun thy_type (dbind, mx, (lhsT, _)) =
+        (dbind, (length o snd o dest_Type) lhsT, mx);
+    val thy = Sign.add_types (map thy_type dom_eqns) thy;
+
+    (* axiomatize type constructor arities *)
+    fun thy_arity (_, _, (lhsT, _)) =
+        let val (dname, tvars) = dest_Type lhsT;
+        in (dname, map (snd o dest_TFree) tvars, @{sort pcpo}) end;
+    val thy = fold (AxClass.axiomatize_arity o thy_arity) dom_eqns thy;
+
     (* declare and axiomatize abs/rep *)
     val (iso_infos, thy) =
-        fold_map axiomatize_isomorphism dom_eqns thy;
+        fold_map axiomatize_isomorphism
+          (map (fn (dbind, _, eqn) => (dbind, eqn)) dom_eqns) thy;
 
     (* define take functions *)
     val (take_info, thy) =
         Domain_Take_Proofs.define_take_functions
-          (map fst dom_eqns ~~ iso_infos) thy;
+          (dbinds ~~ iso_infos) thy;
 
     (* declare lub_take axioms *)
     val (lub_take_thms, thy) =
         fold_map axiomatize_lub_take
-          (map fst dom_eqns ~~ #take_consts take_info) thy;
+          (dbinds ~~ #take_consts take_info) thy;
 
     (* prove additional take theorems *)
     val (take_info2, thy) =
         Domain_Take_Proofs.add_lub_take_theorems
-          (map fst dom_eqns ~~ iso_infos) take_info lub_take_thms thy;
+          (dbinds ~~ iso_infos) take_info lub_take_thms thy;
 
     (* define map functions *)
     val (map_info, thy) =
         Domain_Isomorphism.define_map_functions
-          (map fst dom_eqns ~~ iso_infos) thy;
+          (dbinds ~~ iso_infos) thy;
 
   in
     ((iso_infos, take_info2), thy)

--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Mon Apr 12 13:19:28 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Mon Apr 12 15:05:42 2010 -0700
@@ -142,17 +142,15 @@
                 (dname, map readTFree vs, mx)) eqs'''
       end;
 
-    (* declare new types *)
-    val thy =
-      let
-        fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
-        fun thy_arity (dname,tvars,mx) =
-            (Sign.full_name thy dname, map (snd o dest_TFree) tvars, pcpoS);
-      in
-        thy
-          |> Sign.add_types (map thy_type dtnvs)
-          |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs
-      end;
+    fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
+    fun thy_arity (dname,tvars,mx) =
+      (Sign.full_name thy dname, map (snd o dest_TFree) tvars, @{sort rep});
+
+    (* this theory is used just for parsing and error checking *)
+    val tmp_thy = thy
+      |> Theory.copy
+      |> Sign.add_types (map thy_type dtnvs)
+      |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
 
     val dbinds : binding list =
         map (fn (_,dbind,_,_) => dbind) eqs''';
@@ -161,12 +159,12 @@
         map (fn (_,_,_,cons) => cons) eqs''';
     val cons'' :
         (binding * (bool * binding option * typ) list * mixfix) list list =
-        map (map (upd_second (map (upd_third (prep_typ thy))))) cons''';
+        map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons''';
     val dtnvs' : (string * typ list) list =
       map (fn (dname,vs,mx) => (Sign.full_name thy dname,vs)) dtnvs;
     val eqs' : ((string * typ list) *
         (binding * (bool * binding option * typ) list * mixfix) list) list =
-        check_and_sort_domain false dtnvs' cons'' thy;
+        check_and_sort_domain false dtnvs' cons'' tmp_thy;
     val dts : typ list = map (Type o fst) eqs';
     val new_dts : (string * string list) list =
         map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
@@ -183,9 +181,11 @@
         if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
     fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
     val repTs : typ list = map mk_eq_typ eqs';
-    val dom_eqns : (binding * (typ * typ)) list = dbinds ~~ (dts ~~ repTs);
-    val ((iso_infos, take_info), thy) =
-        Domain_Axioms.add_axioms dom_eqns thy;
+
+    val ((iso_infos, take_info), thy) = thy |>
+        Domain_Axioms.add_axioms
+          (map (fn ((dbind, _, mx), eq) => (dbind, mx, eq))
+            (dtnvs ~~ (dts ~~ repTs)));
 
     val ((rewss, take_rews), theorems_thy) =
         thy