--- 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);
--- 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;
--- 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
--- 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),