--- a/src/HOL/Orderings.thy Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Orderings.thy Sun Nov 08 16:30:41 2009 +0100
@@ -302,7 +302,7 @@
fun struct_eq ((s1: string, ts1), (s2, ts2)) =
(s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
-structure Data = GenericDataFun
+structure Data = Generic_Data
(
type T = ((string * term list) * Order_Tac.less_arith) list;
(* Order structures:
@@ -311,7 +311,7 @@
identifier and operations identify the structure uniquely. *)
val empty = [];
val extend = I;
- fun merge _ = AList.join struct_eq (K fst);
+ fun merge data = AList.join struct_eq (K fst) data;
);
fun print_structures ctxt =