# HG changeset patch
# User wenzelm
# Date 1322840255 -3600
# Node ID 857b7fcb03653874e49edcd8c7c7887821f22a48
# Parent  debb68e8d23f1864f5a9407b9cb32a3da1722731
misc tuning;

diff -r debb68e8d23f -r 857b7fcb0365 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 02 16:24:48 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 02 16:37:35 2011 +0100
@@ -69,10 +69,8 @@
     val thy1 = Sign.add_path big_name thy;
     val big_rec_name = big_name ^ "_rep_set";
     val rep_set_names' =
-      (if length descr' = 1 then [big_rec_name]
-      else
-        (map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
-          (1 upto (length descr'))));
+      if length descr' = 1 then [big_rec_name]
+      else map (prefix (big_rec_name ^ "_") o string_of_int) (1 upto (length descr'));
     val rep_set_names = map (Sign.full_bname thy1) rep_set_names';
 
     val tyvars = map (fn (_, (_, Ts, _)) => map Datatype_Aux.dest_DtTFree Ts) (hd descr);
diff -r debb68e8d23f -r 857b7fcb0365 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Dec 02 16:24:48 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Dec 02 16:37:35 2011 +0100
@@ -103,9 +103,7 @@
     val big_rec_name' = big_name ^ "_rec_set";
     val rec_set_names' =
       if length descr' = 1 then [big_rec_name']
-      else
-        map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
-          (1 upto (length descr'));
+      else map (prefix (big_rec_name' ^ "_") o string_of_int) (1 upto (length descr'));
     val rec_set_names = map (Sign.full_bname thy0) rec_set_names';
 
     val (rec_result_Ts, reccomb_fn_Ts) = Datatype_Prop.make_primrec_Ts descr sorts used;
diff -r debb68e8d23f -r 857b7fcb0365 src/HOL/Tools/Datatype/datatype_aux.ML
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 02 16:24:48 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 02 16:37:35 2011 +0100
@@ -336,7 +336,7 @@
       | SOME {index, descr, ...} =>
           let
             val (_, vars, _) = the (AList.lookup (op =) descr index);
-            val subst = (map dest_DtTFree vars ~~ dts)
+            val subst = map dest_DtTFree vars ~~ dts
               handle ListPair.UnequalLengths =>
                 typ_error T ("Type constructor " ^ tname ^ " used with wrong number of arguments");
           in
diff -r debb68e8d23f -r 857b7fcb0365 src/HOL/Tools/Datatype/datatype_prop.ML
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Dec 02 16:24:48 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Dec 02 16:37:35 2011 +0100
@@ -69,11 +69,12 @@
           val constr_t = Const (cname, Ts ---> T);
           val tnames = make_tnames Ts;
           val frees = map Free (tnames ~~ Ts);
-          val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
-        in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
-          (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
-           foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
-             (map HOLogic.mk_eq (frees ~~ frees')))))
+          val frees' = map Free (map (suffix "'") tnames ~~ Ts);
+        in
+          cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
+            (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
+             foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
+               (map HOLogic.mk_eq (frees ~~ frees')))))
         end;
   in
     map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
@@ -95,7 +96,7 @@
     fun make_distincts' _ [] = []
       | make_distincts' T ((cname, cargs) :: constrs) =
           let
-            val frees = map Free ((make_tnames cargs) ~~ cargs);
+            val frees = map Free (make_tnames cargs ~~ cargs);
             val t = list_comb (Const (cname, cargs ---> T), frees);
 
             fun make_distincts'' (cname', cargs') =
@@ -347,8 +348,7 @@
       end
 
   in
-    map make_split
-      ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr sorts thy "f"))
+    map make_split (hd descr ~~ newTs ~~ make_case_combs new_type_names descr sorts thy "f")
   end;
 
 (************************* additional rules for TFL ***************************)
@@ -400,7 +400,7 @@
           let
             val Ts = binder_types (fastype_of f);
             val tnames = Name.variant_list used (make_tnames Ts);
-            val frees = map Free (tnames ~~ Ts)
+            val frees = map Free (tnames ~~ Ts);
           in
             list_all_free (tnames ~~ Ts, Logic.mk_implies
               (HOLogic.mk_Trueprop
@@ -433,7 +433,7 @@
       let
         val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
         val tnames = Name.variant_list ["v"] (make_tnames Ts);
-        val frees = tnames ~~ Ts
+        val frees = tnames ~~ Ts;
       in
         fold_rev (fn (s, T') => fn t => HOLogic.mk_exists (s, T', t)) frees
           (HOLogic.mk_eq (Free ("v", T),