# HG changeset patch
# User huffman
# Date 1267573987 28800
# Node ID 47eec4da124a79df22e7f8596d4a7215251d3f42
# Parent  f433f18d4c418657cbce77b1ea193cfff5c7f9fe
remove unused mixfix component from type cons

diff -r f433f18d4c41 -r 47eec4da124a src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 15:46:23 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 15:53:07 2010 -0800
@@ -168,7 +168,6 @@
         map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
     fun one_con (con,args,mx) : cons =
         (Binding.name_of con,  (* FIXME preverse binding (!?) *)
-         mx,
          ListPair.map (fn ((lazy,sel,tp),vn) =>
            mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
                       (args, Datatype_Prop.make_tnames (map third args)));
@@ -245,7 +244,6 @@
         map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
     fun one_con (con,args,mx) : cons =
         (Binding.name_of con,   (* FIXME preverse binding (!?) *)
-         mx,
          ListPair.map (fn ((lazy,sel,tp),vn) =>
            mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
                       (args, Datatype_Prop.make_tnames (map third args))
diff -r f433f18d4c41 -r 47eec4da124a src/HOLCF/Tools/Domain/domain_library.ML
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Tue Mar 02 15:46:23 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Tue Mar 02 15:53:07 2010 -0800
@@ -93,7 +93,7 @@
 
       (* Domain specifications *)
       eqtype arg;
-  type cons = string * mixfix * arg list;
+  type cons = string * arg list;
   type eq = (string * typ list) * cons list;
   val mk_arg : (bool * Datatype.dtyp) * string -> arg;
   val is_lazy : arg -> bool;
@@ -189,7 +189,6 @@
 
 type cons =
      string *         (* operator name of constr *)
-     mixfix *         (* mixfix syntax of constructor *)
      arg list;        (* argument list      *)
 
 type eq =
@@ -227,7 +226,7 @@
 fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds;
 
 fun dtyp_of_arg ((lazy, D), _) = if lazy then mk_uD D else D;
-fun dtyp_of_cons (_, _, args) = big_sprodD (map dtyp_of_arg args);
+fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args);
 fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons);
 
 
@@ -331,8 +330,8 @@
                      else mapn (fn n => K("f"^(string_of_int n))) 1 cons;
 fun when_body cons funarg =
     let
-      fun one_fun n (_,_,[]  ) = /\ "dummy" (funarg(1,n))
-        | one_fun n (_,_,args) = let
+      fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
+        | one_fun n (_,args) = let
             val l2 = length args;
             fun idxs m arg = (if is_lazy arg then (fn t => mk_fup (ID, t))
                               else I) (Bound(l2-m));
@@ -342,7 +341,7 @@
                   (args,
                 fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args))))
                ) end;
-    in (if length cons = 1 andalso length(third(hd cons)) <= 1
+    in (if length cons = 1 andalso length(snd (hd cons)) <= 1
         then mk_strictify else I)
          (foldr1 mk_sscase (mapn one_fun 1 cons)) end;
 
diff -r f433f18d4c41 -r 47eec4da124a src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 15:46:23 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 15:53:07 2010 -0800
@@ -179,7 +179,7 @@
   fun get_take_strict dn = PureThy.get_thm thy (dn ^ ".take_strict");
   val axs_take_strict = map get_take_strict dnames;
 
-  fun one_take_app (con, _, args) =
+  fun one_take_app (con, args) =
     let
       fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
       fun one_rhs arg =
@@ -263,7 +263,7 @@
   val dnames = map (fst o fst) eqs;
   val x_name = idx_name dnames "x"; 
 
-  fun one_con (con, _, args) =
+  fun one_con (con, args) =
     let
       val nonrec_args = filter_out is_rec args;
       val    rec_args = filter is_rec args;
@@ -343,7 +343,7 @@
     maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
 
 local
-  fun one_con p (con, _, args) =
+  fun one_con p (con, args) =
     let
       val P_names = map P_name (1 upto (length dnames));
       val vns = Name.variant_list P_names (map vname args);
@@ -367,7 +367,7 @@
   fun ind_prems_tac prems = EVERY
     (maps (fn cons =>
       (resolve_tac prems 1 ::
-        maps (fn (_,_,args) => 
+        maps (fn (_,args) => 
           resolve_tac prems 1 ::
           map (K(atac 1)) (nonlazy args) @
           map (K(atac 1)) (filter is_rec args))
@@ -382,7 +382,7 @@
           ((rec_of arg =  n andalso nfn(lazy_rec orelse is_lazy arg)) orelse 
             rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) 
               (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
-          ) o third) cons;
+          ) o snd) cons;
     fun all_rec_to ns  = rec_to forall not all_rec_to  ns;
     fun warn (n,cons) =
       if all_rec_to [] false (n,cons)
@@ -414,7 +414,7 @@
                         (* FIXME! case_UU_tac *)
             case_UU_tac context (prems @ con_rews) 1
               (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
-          fun con_tacs (con, _, args) = 
+          fun con_tacs (con, args) = 
             asm_simp_tac take_ss 1 ::
             map arg_tac (filter is_nonlazy_rec args) @
             [resolve_tac prems 1] @
@@ -490,7 +490,7 @@
               etac disjE 1,
               asm_simp_tac (HOL_ss addsimps con_rews) 1,
               asm_simp_tac take_ss 1];
-            fun con_tacs ctxt (con, _, args) =
+            fun con_tacs ctxt (con, args) =
               asm_simp_tac take_ss 1 ::
               maps (arg_tacs ctxt) (nonlazy_rec args);
             fun foo_tacs ctxt n (cons, cases) =