merged

--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Mon Feb 22 19:31:18 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Mon Feb 22 11:19:15 2010 -0800
@@ -10,28 +10,25 @@
 
 domain 'a seq = nil  ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq")  (infixr "##" 65)
 
-consts
+(*
    sfilter       :: "('a -> tr) -> 'a seq -> 'a seq"
    smap          :: "('a -> 'b) -> 'a seq -> 'b seq"
    sforall       :: "('a -> tr) => 'a seq => bool"
    sforall2      :: "('a -> tr) -> 'a seq -> tr"
    slast         :: "'a seq     -> 'a"
    sconc         :: "'a seq     -> 'a seq -> 'a seq"
-   sdropwhile    ::"('a -> tr)  -> 'a seq -> 'a seq"
-   stakewhile    ::"('a -> tr)  -> 'a seq -> 'a seq"
-   szip          ::"'a seq      -> 'b seq -> ('a*'b) seq"
+   sdropwhile    :: "('a -> tr)  -> 'a seq -> 'a seq"
+   stakewhile    :: "('a -> tr)  -> 'a seq -> 'a seq"
+   szip          :: "'a seq      -> 'b seq -> ('a*'b) seq"
    sflat        :: "('a seq) seq  -> 'a seq"
 
    sfinite       :: "'a seq set"
-   Partial       ::"'a seq => bool"
-   Infinite      ::"'a seq => bool"
+   Partial       :: "'a seq => bool"
+   Infinite      :: "'a seq => bool"
 
    nproj        :: "nat => 'a seq => 'a"
    sproj        :: "nat => 'a seq => 'a seq"
-
-abbreviation
-  sconc_syn :: "'a seq => 'a seq => 'a seq"  (infixr "@@" 65) where
-  "xs @@ ys == sconc $ xs $ ys"
+*)
 
 inductive
   Finite :: "'a seq => bool"
@@ -39,321 +36,152 @@
     sfinite_0:  "Finite nil"
   | sfinite_n:  "[| Finite tr; a~=UU |] ==> Finite (a##tr)"
 
-defs
-
-(* f not possible at lhs, as "pattern matching" only for % x arguments,
-   f cannot be written at rhs in front, as fix_eq3 does not apply later *)
-smap_def:
-  "smap == (fix$(LAM h f tr. case tr of
-      nil   => nil
-    | x##xs => f$x ## h$f$xs))"
-
-sfilter_def:
-  "sfilter == (fix$(LAM h P t. case t of
-           nil => nil
-         | x##xs => If P$x
-                    then x##(h$P$xs)
-                    else     h$P$xs
-                    fi))"
-sforall_def:
-  "sforall P t == (sforall2$P$t ~=FF)"
-
-
-sforall2_def:
-  "sforall2 == (fix$(LAM h P t. case t of
-           nil => TT
-         | x##xs => P$x andalso h$P$xs))"
-
-sconc_def:
-  "sconc == (fix$(LAM h t1 t2. case t1 of
-               nil       => t2
-             | x##xs => x##(h$xs$t2)))"
+declare Finite.intros [simp]
 
-slast_def:
-  "slast == (fix$(LAM h t. case t of
-           nil => UU
-         | x##xs => (If is_nil$xs
-                          then x
-                         else h$xs fi)))"
-
-stakewhile_def:
-  "stakewhile == (fix$(LAM h P t. case t of
-           nil => nil
-         | x##xs => If P$x
-                    then x##(h$P$xs)
-                    else nil
-                    fi))"
-sdropwhile_def:
-  "sdropwhile == (fix$(LAM h P t. case t of
-           nil => nil
-         | x##xs => If P$x
-                    then h$P$xs
-                    else t
-                    fi))"
-sflat_def:
-  "sflat == (fix$(LAM h t. case t of
-           nil => nil
-         | x##xs => x @@ (h$xs)))"
-
-szip_def:
-  "szip == (fix$(LAM h t1 t2. case t1 of
-               nil   => nil
-             | x##xs => (case t2 of
-                          nil => UU
-                        | y##ys => <x,y>##(h$xs$ys))))"
-
-Partial_def:
+definition
+  Partial :: "'a seq => bool"
+where
   "Partial x  == (seq_finite x) & ~(Finite x)"
 
-Infinite_def:
+definition
+  Infinite :: "'a seq => bool"
+where
   "Infinite x == ~(seq_finite x)"
 
 
-declare Finite.intros [simp]
-
-
 subsection {* recursive equations of operators *}
 
 subsubsection {* smap *}
 
-lemma smap_unfold:
-  "smap = (LAM f tr. case tr of nil  => nil | x##xs => f$x ## smap$f$xs)"
-by (subst fix_eq2 [OF smap_def], simp)
-
-lemma smap_nil [simp]: "smap$f$nil=nil"
-by (subst smap_unfold, simp)
+fixrec
+  smap :: "('a -> 'b) -> 'a seq -> 'b seq"
+where
+  smap_nil: "smap$f$nil=nil"
+| smap_cons: "[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs"
 
 lemma smap_UU [simp]: "smap$f$UU=UU"
-by (subst smap_unfold, simp)
-
-lemma smap_cons [simp]: "[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs"
-apply (rule trans)
-apply (subst smap_unfold)
-apply simp
-apply (rule refl)
-done
+by fixrec_simp
 
 subsubsection {* sfilter *}
 
-lemma sfilter_unfold:
-  "sfilter = (LAM P tr. case tr of
-           nil   => nil
-         | x##xs => If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)"
-by (subst fix_eq2 [OF sfilter_def], simp)
-
-lemma sfilter_nil [simp]: "sfilter$P$nil=nil"
-by (subst sfilter_unfold, simp)
+fixrec
+   sfilter :: "('a -> tr) -> 'a seq -> 'a seq"
+where
+  sfilter_nil: "sfilter$P$nil=nil"
+| sfilter_cons:
+    "x~=UU ==> sfilter$P$(x##xs)=
+              (If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)"
 
 lemma sfilter_UU [simp]: "sfilter$P$UU=UU"
-by (subst sfilter_unfold, simp)
-
-lemma sfilter_cons [simp]:
-"x~=UU ==> sfilter$P$(x##xs)=
-              (If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)"
-apply (rule trans)
-apply (subst sfilter_unfold)
-apply simp
-apply (rule refl)
-done
+by fixrec_simp
 
 subsubsection {* sforall2 *}
 
-lemma sforall2_unfold:
-   "sforall2 = (LAM P tr. case tr of
-                           nil   => TT
-                         | x##xs => (P$x andalso sforall2$P$xs))"
-by (subst fix_eq2 [OF sforall2_def], simp)
-
-lemma sforall2_nil [simp]: "sforall2$P$nil=TT"
-by (subst sforall2_unfold, simp)
+fixrec
+  sforall2 :: "('a -> tr) -> 'a seq -> tr"
+where
+  sforall2_nil: "sforall2$P$nil=TT"
+| sforall2_cons:
+    "x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)"
 
 lemma sforall2_UU [simp]: "sforall2$P$UU=UU"
-by (subst sforall2_unfold, simp)
+by fixrec_simp
 
-lemma sforall2_cons [simp]:
-"x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)"
-apply (rule trans)
-apply (subst sforall2_unfold)
-apply simp
-apply (rule refl)
-done
-
+definition
+  sforall_def: "sforall P t == (sforall2$P$t ~=FF)"
 
 subsubsection {* stakewhile *}
 
-lemma stakewhile_unfold:
-  "stakewhile = (LAM P tr. case tr of
-     nil   => nil
-   | x##xs => (If P$x then x##(stakewhile$P$xs) else nil fi))"
-by (subst fix_eq2 [OF stakewhile_def], simp)
-
-lemma stakewhile_nil [simp]: "stakewhile$P$nil=nil"
-apply (subst stakewhile_unfold)
-apply simp
-done
+fixrec
+  stakewhile :: "('a -> tr)  -> 'a seq -> 'a seq"
+where
+  stakewhile_nil: "stakewhile$P$nil=nil"
+| stakewhile_cons:
+    "x~=UU ==> stakewhile$P$(x##xs) =
+              (If P$x then x##(stakewhile$P$xs) else nil fi)"
 
 lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU"
-apply (subst stakewhile_unfold)
-apply simp
-done
-
-lemma stakewhile_cons [simp]:
-"x~=UU ==> stakewhile$P$(x##xs) =
-              (If P$x then x##(stakewhile$P$xs) else nil fi)"
-apply (rule trans)
-apply (subst stakewhile_unfold)
-apply simp
-apply (rule refl)
-done
+by fixrec_simp
 
 subsubsection {* sdropwhile *}
 
-lemma sdropwhile_unfold:
-   "sdropwhile = (LAM P tr. case tr of
-                           nil   => nil
-                         | x##xs => (If P$x then sdropwhile$P$xs else tr fi))"
-by (subst fix_eq2 [OF sdropwhile_def], simp)
-
-lemma sdropwhile_nil [simp]: "sdropwhile$P$nil=nil"
-apply (subst sdropwhile_unfold)
-apply simp
-done
+fixrec
+  sdropwhile :: "('a -> tr) -> 'a seq -> 'a seq"
+where
+  sdropwhile_nil: "sdropwhile$P$nil=nil"
+| sdropwhile_cons:
+    "x~=UU ==> sdropwhile$P$(x##xs) =
+              (If P$x then sdropwhile$P$xs else x##xs fi)"
 
 lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU"
-apply (subst sdropwhile_unfold)
-apply simp
-done
-
-lemma sdropwhile_cons [simp]:
-"x~=UU ==> sdropwhile$P$(x##xs) =
-              (If P$x then sdropwhile$P$xs else x##xs fi)"
-apply (rule trans)
-apply (subst sdropwhile_unfold)
-apply simp
-apply (rule refl)
-done
-
+by fixrec_simp
 
 subsubsection {* slast *}
 
-lemma slast_unfold:
-   "slast = (LAM tr. case tr of
-                           nil   => UU
-                         | x##xs => (If is_nil$xs then x else slast$xs fi))"
-by (subst fix_eq2 [OF slast_def], simp)
-
-lemma slast_nil [simp]: "slast$nil=UU"
-apply (subst slast_unfold)
-apply simp
-done
+fixrec
+  slast :: "'a seq -> 'a"
+where
+  slast_nil: "slast$nil=UU"
+| slast_cons:
+    "x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)"
 
 lemma slast_UU [simp]: "slast$UU=UU"
-apply (subst slast_unfold)
-apply simp
-done
-
-lemma slast_cons [simp]:
-"x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)"
-apply (rule trans)
-apply (subst slast_unfold)
-apply simp
-apply (rule refl)
-done
-
+by fixrec_simp
 
 subsubsection {* sconc *}
 
-lemma sconc_unfold:
-   "sconc = (LAM t1 t2. case t1 of
-                           nil   => t2
-                         | x##xs => x ## (xs @@ t2))"
-by (subst fix_eq2 [OF sconc_def], simp)
+fixrec
+  sconc :: "'a seq -> 'a seq -> 'a seq"
+where
+  sconc_nil: "sconc$nil$y = y"
+| sconc_cons':
+    "x~=UU ==> sconc$(x##xs)$y = x##(sconc$xs$y)"
 
-lemma sconc_nil [simp]: "nil @@ y = y"
-apply (subst sconc_unfold)
-apply simp
-done
+abbreviation
+  sconc_syn :: "'a seq => 'a seq => 'a seq"  (infixr "@@" 65) where
+  "xs @@ ys == sconc $ xs $ ys"
 
 lemma sconc_UU [simp]: "UU @@ y=UU"
-apply (subst sconc_unfold)
-apply simp
-done
+by fixrec_simp
 
 lemma sconc_cons [simp]: "(x##xs) @@ y=x##(xs @@ y)"
-apply (rule trans)
-apply (subst sconc_unfold)
-apply simp
-apply (case_tac "x=UU")
+apply (cases "x=UU")
 apply simp_all
 done
 
+declare sconc_cons' [simp del]
 
 subsubsection {* sflat *}
 
-lemma sflat_unfold:
-   "sflat = (LAM tr. case tr of
-                           nil   => nil
-                         | x##xs => x @@ sflat$xs)"
-by (subst fix_eq2 [OF sflat_def], simp)
-
-lemma sflat_nil [simp]: "sflat$nil=nil"
-apply (subst sflat_unfold)
-apply simp
-done
+fixrec
+  sflat :: "('a seq) seq -> 'a seq"
+where
+  sflat_nil: "sflat$nil=nil"
+| sflat_cons': "x~=UU ==> sflat$(x##xs)= x@@(sflat$xs)"
 
 lemma sflat_UU [simp]: "sflat$UU=UU"
-apply (subst sflat_unfold)
-apply simp
-done
+by fixrec_simp
 
 lemma sflat_cons [simp]: "sflat$(x##xs)= x@@(sflat$xs)"
-apply (rule trans)
-apply (subst sflat_unfold)
-apply simp
-apply (case_tac "x=UU")
-apply simp_all
-done
+by (cases "x=UU", simp_all)
 
+declare sflat_cons' [simp del]
 
 subsubsection {* szip *}
 
-lemma szip_unfold:
-   "szip = (LAM t1 t2. case t1 of
-                nil   => nil
-              | x##xs => (case t2 of
-                           nil => UU
-                         | y##ys => <x,y>##(szip$xs$ys)))"
-by (subst fix_eq2 [OF szip_def], simp)
-
-lemma szip_nil [simp]: "szip$nil$y=nil"
-apply (subst szip_unfold)
-apply simp
-done
+fixrec
+  szip :: "'a seq -> 'b seq -> ('a*'b) seq"
+where
+  szip_nil: "szip$nil$y=nil"
+| szip_cons_nil: "x~=UU ==> szip$(x##xs)$nil=UU"
+| szip_cons:
+    "[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = <x,y>##szip$xs$ys"
 
 lemma szip_UU1 [simp]: "szip$UU$y=UU"
-apply (subst szip_unfold)
-apply simp
-done
+by fixrec_simp
 
 lemma szip_UU2 [simp]: "x~=nil ==> szip$x$UU=UU"
-apply (subst szip_unfold)
-apply simp
-apply (rule_tac x="x" in seq.casedist)
-apply simp_all
-done
-
-lemma szip_cons_nil [simp]: "x~=UU ==> szip$(x##xs)$nil=UU"
-apply (rule trans)
-apply (subst szip_unfold)
-apply simp_all
-done
-
-lemma szip_cons [simp]:
-"[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = <x,y>##szip$xs$ys"
-apply (rule trans)
-apply (subst szip_unfold)
-apply simp_all
-done
+by (cases x, simp_all, fixrec_simp)
 
 
 subsection "scons, nil"

--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Feb 22 19:31:18 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Feb 22 11:19:15 2010 -0800
@@ -88,23 +88,23 @@
         | inj y i j = mk_sinr (inj y (i-1) (j-1));
     in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end;
           
-    val con_defs = mapn (fn n => fn (con,args) =>
+    val con_defs = mapn (fn n => fn (con, _, args) =>
                                     (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons;
           
     val dis_defs = let
-      fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == 
+      fun ddef (con,_,_) = (dis_name con ^"_def",%%:(dis_name con) == 
                                               list_ccomb(%%:(dname^"_when"),map 
-                                                                              (fn (con',args) => (List.foldr /\#
+                                                                              (fn (con',_,args) => (List.foldr /\#
       (if con'=con then TT else FF) args)) cons))
     in map ddef cons end;
 
     val mat_defs =
       let
-        fun mdef (con,_) =
+        fun mdef (con, _, _) =
           let
             val k = Bound 0
             val x = Bound 1
-            fun one_con (con', args') =
+            fun one_con (con', _, args') =
                 if con'=con then k else List.foldr /\# mk_fail args'
             val w = list_ccomb(%%:(dname^"_when"), map one_con cons)
             val rhs = /\ "x" (/\ "k" (w ` x))
@@ -113,14 +113,14 @@
 
     val pat_defs =
       let
-        fun pdef (con,args) =
+        fun pdef (con, _, args) =
           let
             val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
             val xs = map (bound_arg args) args;
             val r = Bound (length args);
             val rhs = case args of [] => mk_return HOLogic.unit
                                  | _ => mk_ctuple_pat ps ` mk_ctuple xs;
-            fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args';
+            fun one_con (con', _, args') = List.foldr /\# (if con'=con then rhs else mk_fail) args';
           in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == 
                                               list_ccomb(%%:(dname^"_when"), map one_con cons))
           end
@@ -129,9 +129,9 @@
     val sel_defs = let
       fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == 
                                                             list_ccomb(%%:(dname^"_when"),map 
-                                                                                            (fn (con',args) => if con'<>con then UU else
+                                                                                            (fn (con', _, args) => if con'<>con then UU else
                                                                                                                List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
-    in map_filter I (maps (fn (con,args) => mapn (sdef con) 1 args) cons) end;
+    in map_filter I (maps (fn (con, _, args) => mapn (sdef con) 1 args) cons) end;
 
 
 (* ----- axiom and definitions concerning induction ------------------------- *)
@@ -175,7 +175,7 @@
 
 fun add_matchers (((dname,_),cons) : eq) thy =
     let
-      val con_names = map fst cons;
+      val con_names = map first cons;
       val mat_names = map mat_name con_names;
       fun qualify n = Sign.full_name thy (Binding.name n);
       val ms = map qualify con_names ~~ map qualify mat_names;
@@ -190,7 +190,7 @@
     val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
                                  /\ "f"(mk_ctuple (map copy_app dnames)));
 
-    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;

--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Mon Feb 22 19:31:18 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Mon Feb 22 11:19:15 2010 -0800
@@ -161,6 +161,7 @@
       | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
     fun one_con (con,args,mx) =
         (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),
                    Option.map Binding.name_of sel,vn))
@@ -236,6 +237,7 @@
       | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
     fun one_con (con,args,mx) =
         (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),
                    Option.map Binding.name_of sel,vn))

--- a/src/HOLCF/Tools/Domain/domain_library.ML	Mon Feb 22 19:31:18 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Mon Feb 22 11:19:15 2010 -0800
@@ -132,7 +132,7 @@
 
       (* Domain specifications *)
       eqtype arg;
-  type cons = string * arg list;
+  type cons = string * mixfix * arg list;
   type eq = (string * typ list) * cons list;
   val mk_arg : (bool * Datatype.dtyp) * string option * string -> arg;
   val is_lazy : arg -> bool;
@@ -220,6 +220,7 @@
 
 type cons =
      string *         (* operator name of constr *)
+     mixfix *         (* mixfix syntax of constructor *)
      arg list;        (* argument list      *)
 
 type eq =
@@ -258,7 +259,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);
 
 
@@ -377,8 +378,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));
@@ -388,7 +389,7 @@
                   (args,
                 fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args))))
                ) end;
-    in (if length cons = 1 andalso length(snd(hd cons)) <= 1
+    in (if length cons = 1 andalso length(third(hd cons)) <= 1
         then mk_strictify else I)
          (foldr1 mk_sscase (mapn one_fun 1 cons)) end;
 

--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Feb 22 19:31:18 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Feb 22 11:19:15 2010 -0800
@@ -24,8 +24,6 @@
 fun message s = if !quiet_mode then () else writeln s;
 fun trace s = if !trace_domain then tracing s else ();
 
-local
-
 val adm_impl_admw = @{thm adm_impl_admw};
 val adm_all = @{thm adm_all};
 val adm_conj = @{thm adm_conj};
@@ -134,8 +132,6 @@
 
 val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: below_antisym_inverse)}
 
-in
-
 fun theorems (((dname, _), cons) : eq, eqs : eq list) thy =
 let
 
@@ -152,7 +148,7 @@
   val ax_abs_iso  = ga "abs_iso"  dname;
   val ax_rep_iso  = ga "rep_iso"  dname;
   val ax_when_def = ga "when_def" dname;
-  fun get_def mk_name (con,_) = ga (mk_name con^"_def") dname;
+  fun get_def mk_name (con, _, _) = ga (mk_name con^"_def") dname;
   val axs_con_def = map (get_def extern_name) cons;
   val axs_dis_def = map (get_def dis_name) cons;
   val axs_mat_def = map (get_def mat_name) cons;
@@ -161,7 +157,7 @@
     let
       fun def_of_sel sel = ga (sel^"_def") dname;
       fun def_of_arg arg = Option.map def_of_sel (sel_of arg);
-      fun defs_of_con (_, args) = map_filter def_of_arg args;
+      fun defs_of_con (_, _, args) = map_filter def_of_arg args;
     in
       maps defs_of_con cons
     end;
@@ -226,10 +222,10 @@
     in (n2, mk_sprodT (t1, t2)) end;
 
   fun cons2typ n [] = (n,oneT)
-    | cons2typ n [con] = args2typ n (snd con)
+    | cons2typ n [con] = args2typ n (third con)
     | cons2typ n (con::cons) =
     let
-      val (n1, t1) = args2typ n (snd con);
+      val (n1, t1) = args2typ n (third con);
       val (n2, t2) = cons2typ n1 cons
     in (n2, mk_ssumT (t1, t2)) end;
 in
@@ -238,7 +234,7 @@
 
 local 
   val iso_swap = iso_locale RS iso_iso_swap;
-  fun one_con (con, args) =
+  fun one_con (con, _, args) =
     let
       val vns = map vname args;
       val eqn = %:x_name === con_app2 con %: vns;
@@ -282,7 +278,7 @@
   val _ = trace " Proving when_apps...";
   val when_apps =
     let
-      fun one_when n (con,args) =
+      fun one_when n (con, _, args) =
         let
           val axs = when_appl :: con_appls;
           val goal = bind_fun (lift_defined %: (nonlazy args, 
@@ -297,12 +293,12 @@
 (* ----- theorems concerning the constructors, discriminators and selectors - *)
 
 local
-  fun dis_strict (con, _) =
+  fun dis_strict (con, _, _) =
     let
       val goal = mk_trp (strict (%%:(dis_name con)));
     in pg axs_dis_def goal (K [rtac when_strict 1]) end;
 
-  fun dis_app c (con, args) =
+  fun dis_app c (con, _, args) =
     let
       val lhs = %%:(dis_name c) ` con_app con args;
       val rhs = if con = c then TT else FF;
@@ -311,9 +307,9 @@
     in pg axs_dis_def goal (K tacs) end;
 
   val _ = trace " Proving dis_apps...";
-  val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons;
+  val dis_apps = maps (fn (c,_,_) => map (dis_app c) cons) cons;
 
-  fun dis_defin (con, args) =
+  fun dis_defin (con, _, args) =
     let
       val goal = defined (%:x_name) ==> defined (%%:(dis_name con) `% x_name);
       val tacs =
@@ -332,7 +328,7 @@
 end;
 
 local
-  fun mat_strict (con, _) =
+  fun mat_strict (con, _, _) =
     let
       val goal = mk_trp (%%:(mat_name con) ` UU ` %:"rhs" === UU);
       val tacs = [asm_simp_tac (HOLCF_ss addsimps [when_strict]) 1];
@@ -341,7 +337,7 @@
   val _ = trace " Proving mat_stricts...";
   val mat_stricts = map mat_strict cons;
 
-  fun one_mat c (con, args) =
+  fun one_mat c (con, _, args) =
     let
       val lhs = %%:(mat_name c) ` con_app con args ` %:"rhs";
       val rhs =
@@ -354,7 +350,7 @@
 
   val _ = trace " Proving mat_apps...";
   val mat_apps =
-    maps (fn (c,_) => map (one_mat c) cons) cons;
+    maps (fn (c,_,_) => map (one_mat c) cons) cons;
 in
   val mat_rews = mat_stricts @ mat_apps;
 end;
@@ -362,10 +358,10 @@
 local
   fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
 
-  fun pat_lhs (con,args) = mk_branch (list_comb (%%:(pat_name con), ps args));
+  fun pat_lhs (con,_,args) = mk_branch (list_comb (%%:(pat_name con), ps args));
 
-  fun pat_rhs (con,[]) = mk_return ((%:"rhs") ` HOLogic.unit)
-    | pat_rhs (con,args) =
+  fun pat_rhs (con,_,[]) = mk_return ((%:"rhs") ` HOLogic.unit)
+    | pat_rhs (con,_,args) =
         (mk_branch (mk_ctuple_pat (ps args)))
           `(%:"rhs")`(mk_ctuple (map %# args));
 
@@ -376,11 +372,11 @@
       val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1];
     in pg axs goal (K tacs) end;
 
-  fun pat_app c (con, args) =
+  fun pat_app c (con, _, args) =
     let
       val axs = @{thm branch_def} :: axs_pat_def;
       val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args);
-      val rhs = if con = fst c then pat_rhs c else mk_fail;
+      val rhs = if con = first c then pat_rhs c else mk_fail;
       val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
     in pg axs goal (K tacs) end;
@@ -394,7 +390,7 @@
 end;
 
 local
-  fun con_strict (con, args) = 
+  fun con_strict (con, _, args) = 
     let
       val rules = abs_strict :: @{thms con_strict_rules};
       fun one_strict vn =
@@ -405,7 +401,7 @@
         in pg con_appls goal (K tacs) end;
     in map one_strict (nonlazy args) end;
 
-  fun con_defin (con, args) =
+  fun con_defin (con, _, args) =
     let
       fun iff_disj (t, []) = HOLogic.mk_not t
         | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts;
@@ -427,7 +423,7 @@
 local
   val rules =
     [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE];
-  fun con_compact (con, args) =
+  fun con_compact (con, _, args) =
     let
       val concl = mk_trp (mk_compact (con_app con args));
       val goal = lift (fn x => mk_compact (%#x)) (args, concl);
@@ -445,7 +441,7 @@
     pg axs_sel_def (mk_trp (strict (%%:sel)))
       (K [simp_tac (HOLCF_ss addsimps when_rews) 1]);
 
-  fun sel_strict (_, args) =
+  fun sel_strict (_, _, args) =
     map_filter (Option.map one_sel o sel_of) args;
 in
   val _ = trace " Proving sel_stricts...";
@@ -476,14 +472,14 @@
       val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
     in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
 
-  fun sel_app c n sel (con, args) =
+  fun sel_app c n sel (con, _, args) =
     if con = c
     then sel_app_same c n sel (con, args)
     else sel_app_diff c n sel (con, args);
 
   fun one_sel c n sel = map (sel_app c n sel) cons;
   fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg);
-  fun one_con (c, args) =
+  fun one_con (c, _, args) =
     flat (map_filter I (mapn (one_sel' c) 0 args));
 in
   val _ = trace " Proving sel_apps...";
@@ -505,7 +501,7 @@
   val sel_defins =
     if length cons = 1
     then map_filter (fn arg => Option.map sel_defin (sel_of arg))
-                 (filter_out is_lazy (snd (hd cons)))
+                 (filter_out is_lazy (third (hd cons)))
     else [];
 end;
 
@@ -526,7 +522,7 @@
         val tacs = [simp_tac (HOL_ss addsimps rules) 1];
       in pg con_appls goal (K tacs) end;
 
-    fun distinct (con1, args1) (con2, args2) =
+    fun distinct (con1, _, args1) (con2, _, args2) =
         let
           val arg1 = (con1, args1);
           val arg2 =
@@ -558,7 +554,7 @@
         val tacs = [simp_tac (HOL_ss addsimps rules) 1];
       in pg con_appls goal (K tacs) end;
 
-    fun distinct (con1, args1) (con2, args2) =
+    fun distinct (con1, _, args1) (con2, _, args2) =
         let
           val arg1 = (con1, args1);
           val arg2 =
@@ -580,7 +576,7 @@
       val sargs = case largs of [_] => [] | _ => nonlazy args;
       val prop = lift_defined %: (sargs, mk_trp (prem === concl));
     in pg con_appls prop end;
-  val cons' = filter (fn (_,args) => args<>[]) cons;
+  val cons' = filter (fn (_, _, args) => args<>[]) cons;
 in
   val _ = trace " Proving inverts...";
   val inverts =
@@ -588,14 +584,14 @@
       val abs_less = ax_abs_iso RS (allI RS injection_less);
       val tacs =
         [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1];
-    in map (fn (con, args) => pgterm (op <<) con args (K tacs)) cons' end;
+    in map (fn (con, _, args) => pgterm (op <<) con args (K tacs)) cons' end;
 
   val _ = trace " Proving injects...";
   val injects =
     let
       val abs_eq = ax_abs_iso RS (allI RS injection_eq);
       val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1];
-    in map (fn (con, args) => pgterm (op ===) con args (K tacs)) cons' end;
+    in map (fn (con, _, args) => pgterm (op ===) con args (K tacs)) cons' end;
 end;
 
 (* ----- theorems concerning one induction step ----------------------------- *)
@@ -614,7 +610,7 @@
   end;
 
 local
-  fun copy_app (con, args) =
+  fun copy_app (con, _, args) =
     let
       val lhs = dc_copy`%"f"`(con_app con args);
       fun one_rhs arg =
@@ -639,7 +635,7 @@
 end;
 
 local
-  fun one_strict (con, args) = 
+  fun one_strict (con, _, args) = 
     let
       val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
       val rews = the_list copy_strict @ copy_apps @ con_rews;
@@ -652,7 +648,7 @@
       | ERROR s => (trace s; NONE)
     end;
 
-  fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args;
+  fun has_nonlazy_rec (_, _, args) = exists is_nonlazy_rec args;
 in
   val _ = trace " Proving copy_stricts...";
   val copy_stricts = map_filter one_strict (filter has_nonlazy_rec cons);
@@ -753,7 +749,7 @@
     in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
   val take_0s = mapn take_0 1 dnames;
   val _ = trace " Proving take_apps...";
-  fun one_take_app dn (con, args) =
+  fun one_take_app dn (con, _, args) =
     let
       fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
       fun one_rhs arg =
@@ -777,7 +773,7 @@
 end; (* local *)
 
 local
-  fun one_con p (con,args) =
+  fun one_con p (con, _, args) =
     let
       fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
       val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
@@ -798,7 +794,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))
@@ -813,7 +809,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 snd) cons;
+          ) o third) 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)
@@ -844,7 +840,7 @@
           fun arg_tac arg =
             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] @
@@ -931,7 +927,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) =
@@ -1089,5 +1085,4 @@
            else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
        |> Sign.parent_path |> pair take_rews
 end; (* let *)
-end; (* local *)
 end; (* struct *)