# HG changeset patch # User wenzelm # Date 1323719757 -3600 # Node ID c2f6c50e3d42067a70145b7f6531f3a8a493b945 # Parent 1fe2dd6d5086ea389670b8890fbefb21989e0fce tuned; diff -r 1fe2dd6d5086 -r c2f6c50e3d42 src/HOL/Tools/Datatype/datatype.ML --- 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)] diff -r 1fe2dd6d5086 -r c2f6c50e3d42 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- 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); diff -r 1fe2dd6d5086 -r c2f6c50e3d42 src/HOL/Tools/Datatype/datatype_aux.ML --- 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 *) diff -r 1fe2dd6d5086 -r c2f6c50e3d42 src/HOL/Tools/Datatype/datatype_data.ML --- 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; diff -r 1fe2dd6d5086 -r c2f6c50e3d42 src/HOL/Tools/Datatype/datatype_prop.ML --- 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);