merged

--- a/src/HOL/Tools/Datatype/datatype.ML	Mon Oct 12 12:19:19 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Oct 12 14:22:54 2009 +0200
@@ -321,7 +321,7 @@
     split_asm = split_asm});
 
 fun derive_datatype_props config dt_names alt_names descr sorts
-    induct inject (distinct_rules, distinct_rewrites, distinct_entry) thy1 =
+    induct inject distinct thy1 =
   let
     val thy2 = thy1 |> Theory.checkpoint;
     val flat_descr = flat descr;
@@ -334,7 +334,7 @@
       descr sorts exhaust thy3;
     val ((rec_names, rec_rewrites), thy5) = DatatypeAbsProofs.prove_primrec_thms
       config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
-      inject distinct_rewrites (Simplifier.theory_context thy4 dist_ss) induct thy4;
+      inject distinct (Simplifier.theory_context thy4 dist_ss) induct thy4;
     val ((case_rewrites, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
       config new_type_names descr sorts rec_names rec_rewrites thy5;
     val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
@@ -342,15 +342,15 @@
     val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
       descr sorts thy7;
     val (splits, thy9) = DatatypeAbsProofs.prove_split_thms
-      config new_type_names descr sorts inject distinct_rewrites exhaust case_rewrites thy8;
+      config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
 
     val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
     val dt_infos = map_index (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
-      (hd descr ~~ inject ~~ distinct_entry ~~ exhaust ~~ nchotomys ~~
+      (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
         case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
     val dt_names = map fst dt_infos;
     val prfx = Binding.qualify true (space_implode "_" new_type_names);
-    val simps = flat (inject @ distinct_rules @ case_rewrites) @ rec_rewrites;
+    val simps = flat (inject @ distinct @ case_rewrites) @ rec_rewrites;
     val named_rules = flat (map_index (fn (index, tname) =>
       [((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
        ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
@@ -362,11 +362,11 @@
     |> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []),
         ((prfx (Binding.name "inducts"), inducts), []),
         ((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []),
-        ((Binding.empty, flat case_rewrites @ flat distinct_rules @ rec_rewrites),
+        ((Binding.empty, flat case_rewrites @ flat distinct @ rec_rewrites),
           [Simplifier.simp_add]),
         ((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]),
         ((Binding.empty, flat inject), [iff_add]),
-        ((Binding.empty, map (fn th => th RS notE) (flat distinct_rules)),
+        ((Binding.empty, map (fn th => th RS notE) (flat distinct)),
           [Classical.safe_elim NONE]),
         ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)])]
         @ named_rules @ unnamed_rules)
@@ -394,7 +394,7 @@
   in
     thy2
     |> derive_datatype_props config dt_names alt_names [descr] sorts
-         induct inject (distinct, distinct, distinct)
+         induct inject distinct
  end;
 
 fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
@@ -531,12 +531,12 @@
       else raise exn;
 
     val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
-    val ((inject, (distinct_rules, distinct_rewrites, distinct_entry), induct), thy') = thy |>
+    val ((inject, distinct, induct), thy') = thy |>
       DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
         types_syntax constr_syntax (mk_case_names_induct (flat descr));
   in
     derive_datatype_props config dt_names (SOME new_type_names) descr sorts
-      induct inject (distinct_rules, distinct_rewrites, distinct_entry) thy'
+      induct inject distinct thy'
   end;
 
 val add_datatype = gen_add_datatype cert_typ;

--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Oct 12 12:19:19 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Oct 12 14:22:54 2009 +0200
@@ -65,8 +65,8 @@
         val insts = Library.take (i, dummyPs) @ (P::(Library.drop (i + 1, dummyPs)));
         val cert = cterm_of thy;
         val insts' = (map cert induct_Ps) ~~ (map cert insts);
-        val induct' = refl RS ((List.nth
-          (split_conj_thm (cterm_instantiate insts' induct), i)) RSN (2, rev_mp))
+        val induct' = refl RS ((nth
+          (split_conj_thm (cterm_instantiate insts' induct)) i) RSN (2, rev_mp))
 
       in
         SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
@@ -123,17 +123,17 @@
 
     (* introduction rules for graph of primrec function *)
 
-    fun make_rec_intr T rec_set ((rec_intr_ts, l), (cname, cargs)) =
+    fun make_rec_intr T rec_set (cname, cargs) (rec_intr_ts, l) =
       let
         fun mk_prem ((dt, U), (j, k, prems, t1s, t2s)) =
           let val free1 = mk_Free "x" U j
           in (case (strip_dtyp dt, strip_type U) of
              ((_, DtRec m), (Us, _)) =>
                let
-                 val free2 = mk_Free "y" (Us ---> List.nth (rec_result_Ts, m)) k;
+                 val free2 = mk_Free "y" (Us ---> nth rec_result_Ts m) k;
                  val i = length Us
                in (j + 1, k + 1, HOLogic.mk_Trueprop (HOLogic.list_all
-                     (map (pair "x") Us, List.nth (rec_sets', m) $
+                     (map (pair "x") Us, nth rec_sets' m $
                        app_bnds free1 i $ app_bnds free2 i)) :: prems,
                    free1::t1s, free2::t2s)
                end
@@ -145,12 +145,12 @@
 
       in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop
         (rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $
-          list_comb (List.nth (rec_fns, l), t1s @ t2s)))], l + 1)
+          list_comb (nth rec_fns l, t1s @ t2s)))], l + 1)
       end;
 
-    val (rec_intr_ts, _) = Library.foldl (fn (x, ((d, T), set_name)) =>
-      Library.foldl (make_rec_intr T set_name) (x, #3 (snd d)))
-        (([], 0), descr' ~~ recTs ~~ rec_sets');
+    val (rec_intr_ts, _) = fold (fn ((d, T), set_name) =>
+      fold (make_rec_intr T set_name) (#3 (snd d)))
+        (descr' ~~ recTs ~~ rec_sets') ([], 0);
 
     val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
         Inductive.add_inductive_global (serial_string ())
@@ -165,18 +165,18 @@
 
     val _ = message config "Proving termination and uniqueness of primrec functions ...";
 
-    fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) =
+    fun mk_unique_tac ((((i, (tname, _, constrs)), elim), T), T') (tac, intrs) =
       let
         val distinct_tac =
           (if i < length newTs then
-             full_simp_tac (HOL_ss addsimps (List.nth (dist_rewrites, i))) 1
+             full_simp_tac (HOL_ss addsimps (nth dist_rewrites i)) 1
            else full_simp_tac dist_ss 1);
 
         val inject = map (fn r => r RS iffD1)
-          (if i < length newTs then List.nth (constr_inject, i)
+          (if i < length newTs then nth constr_inject i
             else injects_of tname);
 
-        fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) =
+        fun mk_unique_constr_tac n (cname, cargs) (tac, intr::intrs, j) =
           let
             val k = length (filter is_rec_type cargs)
 
@@ -195,8 +195,8 @@
               intrs, j + 1)
           end;
 
-        val (tac', intrs', _) = Library.foldl (mk_unique_constr_tac (length constrs))
-          ((tac, intrs, 0), constrs);
+        val (tac', intrs', _) = fold (mk_unique_constr_tac (length constrs))
+          constrs (tac, intrs, 0);
 
       in (tac', intrs') end;
 
@@ -211,10 +211,9 @@
           ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
         val induct' = cterm_instantiate ((map cert induct_Ps) ~~
           (map cert insts)) induct;
-        val (tac, _) = Library.foldl mk_unique_tac
-          (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
-              THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs),
-            descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
+        val (tac, _) = fold mk_unique_tac (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
+           (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
+              THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs));
 
       in split_conj_thm (SkipProof.prove_global thy1 [] []
         (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
@@ -267,7 +266,7 @@
          [Nitpick_Const_Simps.add])]
     ||> Sign.parent_path
     ||> Theory.checkpoint
-    |-> (fn thms => pair (reccomb_names, Library.flat thms))
+    |-> (fn thms => pair (reccomb_names, flat thms))
   end;
 
 
@@ -298,10 +297,9 @@
 
     (* define case combinators via primrec combinators *)
 
-    val (case_defs, thy2) = Library.foldl (fn ((defs, thy),
-      ((((i, (_, _, constrs)), T), name), recname)) =>
+    val (case_defs, thy2) = fold (fn ((((i, (_, _, constrs)), T), name), recname) => fn (defs, thy) =>
         let
-          val (fns1, fns2) = ListPair.unzip (map (fn ((_, cargs), j) =>
+          val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
             let
               val Ts = map (typ_of_dtyp descr' sorts) cargs;
               val Ts' = Ts @ map mk_dummyT (List.filter is_rec_type cargs);
@@ -328,8 +326,8 @@
             |> (PureThy.add_defs false o map Thm.no_attributes) [def];
 
         in (defs @ [def_thm], thy')
-        end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
-          (Library.take (length newTs, reccomb_names)))
+        end) (hd descr ~~ newTs ~~ case_names ~~
+          Library.take (length newTs, reccomb_names)) ([], thy1)
       ||> Theory.checkpoint;
 
     val case_thms = map (map (fn t => SkipProof.prove_global thy2 [] [] t

--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Mon Oct 12 12:19:19 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Mon Oct 12 14:22:54 2009 +0200
@@ -15,8 +15,7 @@
   val representation_proofs : config -> info Symtab.table ->
     string list -> descr list -> (string * sort) list ->
       (binding * mixfix) list -> (binding * mixfix) list list -> attribute
-        -> theory -> (thm list list * (thm list list * thm list list *
-          thm list list) * thm) * theory
+        -> theory -> (thm list list * thm list list * thm) * theory
 end;
 
 structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
@@ -618,7 +617,7 @@
       ||> Theory.checkpoint;
 
   in
-    ((constr_inject', (distinct_thms', dist_rewrites, distinct_thms'), dt_induct'), thy7)
+    ((constr_inject', distinct_thms', dt_induct'), thy7)
   end;
 
 end;