src/HOL/HOL.ML
changeset 1668 8ead1fe65aad
parent 1660 8cb42cd97579
child 1672 2c109cd2fdd0
     1.1 --- a/src/HOL/HOL.ML	Fri Apr 19 11:18:59 1996 +0200
     1.2 +++ b/src/HOL/HOL.ML	Fri Apr 19 11:33:24 1996 +0200
     1.3 @@ -408,12 +408,17 @@
     1.4       ("simpset", ThyMethods {merge = merge, put = put, get = get})
     1.5  end;
     1.6  
     1.7 -exception DT_DATA of string list;
     1.8 -val datatypes = ref [] : string list ref;
     1.9 +
    1.10 +type dtype_info = {case_const:term, case_rewrites:thm list,
    1.11 +                   constructors:term list, nchotomy:thm, case_cong:thm};
    1.12 +
    1.13 +exception DT_DATA of (string * dtype_info) list;
    1.14 +val datatypes = ref [] : (string * dtype_info) list ref;
    1.15  
    1.16  let fun merge [] = DT_DATA []
    1.17 -      | merge ds = let val ds = map (fn DT_DATA x => x) ds;
    1.18 -                   in DT_DATA (foldl (op union) (hd ds, tl ds)) end;
    1.19 +      | merge ds =
    1.20 +          let val ds = map (fn DT_DATA x => x) ds;
    1.21 +          in DT_DATA (foldl (gen_union eq_fst) (hd ds, tl ds)) end;
    1.22  
    1.23      fun put (DT_DATA ds) = datatypes := ds;
    1.24