--- a/src/HOL/Tools/Datatype/datatype.ML Mon Dec 12 19:47:50 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Mon Dec 12 20:55:57 2011 +0100
@@ -70,7 +70,7 @@
val big_rec_name = big_name ^ "_rep_set";
val rep_set_names' =
if length descr' = 1 then [big_rec_name]
- else map (prefix (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 rep_set_names = map (Sign.full_bname thy1) rep_set_names';
val tyvars = map (fn (_, (_, Ts, _)) => map Datatype_Aux.dest_DtTFree Ts) (hd descr);
@@ -111,8 +111,8 @@
val Type (_, [T1, T2]) = T;
in
if i <= n2
- then Const (@{const_name Inl}, T1 --> T) $ (mk_inj' T1 n2 i)
- else Const (@{const_name Inr}, T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
+ then Const (@{const_name Inl}, T1 --> T) $ mk_inj' T1 n2 i
+ else Const (@{const_name Inr}, T2 --> T) $ mk_inj' T2 (n - n2) (i - n2)
end;
in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs) end;
@@ -175,7 +175,7 @@
val intr_ts = maps (fn ((_, (_, _, constrs)), rep_set_name) =>
map (make_intr rep_set_name (length constrs))
- ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names');
+ ((1 upto length constrs) ~~ constrs)) (descr' ~~ rep_set_names');
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
thy1
@@ -242,8 +242,8 @@
val rhs = mk_univ_inj r_args n i;
val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs);
val def_name = Long_Name.base_name cname ^ "_def";
- val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
- (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
+ val eqn =
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
val ([def_thm], thy') =
thy
|> Sign.add_consts_i [(cname', constrT, mx)]
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Dec 12 19:47:50 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Dec 12 20:55:57 2011 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Tools/Datatype/datatype_abs_proofs.ML
Author: Stefan Berghofer, TU Muenchen
-Datatype package: proofs and defintions independent of concrete
+Datatype package: proofs and definitions independent of concrete
representation of datatypes (i.e. requiring only abstract
properties: injectivity / distinctness of constructors and induction).
*)
@@ -103,7 +103,7 @@
val big_rec_name' = big_name ^ "_rec_set";
val rec_set_names' =
if length descr' = 1 then [big_rec_name']
- else map (prefix (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;
@@ -112,7 +112,7 @@
map (fn (T1, T2) => (reccomb_fn_Ts @ [T1, T2]) ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
val rec_fns =
- map (uncurry (Datatype_Aux.mk_Free "f")) (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
+ map (uncurry (Datatype_Aux.mk_Free "f")) (reccomb_fn_Ts ~~ (1 upto length reccomb_fn_Ts));
val rec_sets' =
map (fn c => list_comb (Free c, rec_fns)) (rec_set_names' ~~ rec_set_Ts);
val rec_sets =
@@ -136,7 +136,7 @@
Datatype_Aux.app_bnds free1 i $ Datatype_Aux.app_bnds free2 i)) :: prems,
free1 :: t1s, free2 :: t2s)
end
- | _ => (j + 1, k, prems, free1::t1s, t2s))
+ | _ => (j + 1, k, prems, free1 :: t1s, t2s))
end;
val Ts = map (Datatype_Aux.typ_of_dtyp descr' sorts) cargs;
@@ -233,7 +233,7 @@
val reccomb_names =
map (Sign.full_bname thy1)
(if length descr' = 1 then [big_reccomb_name]
- else map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto (length descr')));
+ else map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto length descr'));
val reccombs =
map (fn ((name, T), T') => list_comb (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
(reccomb_names ~~ recTs ~~ rec_result_Ts);
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Mon Dec 12 19:47:50 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Mon Dec 12 20:55:57 2011 +0100
@@ -177,7 +177,7 @@
datatype dtyp =
DtTFree of string
- | DtType of string * (dtyp list)
+ | DtType of string * dtyp list
| DtRec of int;
(* information about datatypes *)
--- a/src/HOL/Tools/Datatype/datatype_data.ML Mon Dec 12 19:47:50 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon Dec 12 20:55:57 2011 +0100
@@ -69,7 +69,7 @@
fun info_of_constr thy (c, T) =
let
- val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
+ val tab = Symtab.lookup_list (#constrs (DatatypesData.get thy)) c;
in
(case body_type T of
Type (tyco, _) => AList.lookup (op =) tab tyco
@@ -109,8 +109,8 @@
fun the_spec thy dtco =
let
- val { descr, index, sorts = raw_sorts, ... } = the_info thy dtco;
- val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index;
+ val {descr, index, sorts = raw_sorts, ...} = the_info thy dtco;
+ val (_, dtys, raw_cos) = the (AList.lookup (op =) descr index);
val sorts =
map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v)) o Datatype_Aux.dest_DtTFree) dtys;
val cos = map (fn (co, tys) => (co, map (Datatype_Aux.typ_of_dtyp descr sorts) tys)) raw_cos;
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Mon Dec 12 19:47:50 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Mon Dec 12 20:55:57 2011 +0100
@@ -230,7 +230,7 @@
val reccomb_names =
map (Sign.intern_const thy)
(if length descr' = 1 then [big_reccomb_name]
- else (map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto (length descr'))));
+ else (map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto length descr')));
val reccombs =
map (fn ((name, T), T') => list_comb (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
(reccomb_names ~~ recTs ~~ rec_result_Ts);