src/HOL/Orderings.thy
changeset 33519 e31a85f92ce9
parent 32960 69916a850301
child 34065 6f8f9835e219
     1.1 --- a/src/HOL/Orderings.thy	Sun Nov 08 16:28:18 2009 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Sun Nov 08 16:30:41 2009 +0100
     1.3 @@ -302,7 +302,7 @@
     1.4  fun struct_eq ((s1: string, ts1), (s2, ts2)) =
     1.5    (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
     1.6  
     1.7 -structure Data = GenericDataFun
     1.8 +structure Data = Generic_Data
     1.9  (
    1.10    type T = ((string * term list) * Order_Tac.less_arith) list;
    1.11      (* Order structures:
    1.12 @@ -311,7 +311,7 @@
    1.13         identifier and operations identify the structure uniquely. *)
    1.14    val empty = [];
    1.15    val extend = I;
    1.16 -  fun merge _ = AList.join struct_eq (K fst);
    1.17 +  fun merge data = AList.join struct_eq (K fst) data;
    1.18  );
    1.19  
    1.20  fun print_structures ctxt =