
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Orderings.thy
--- 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 =




