diff -r d064fa48f305 -r 24563731b9b2 src/HOL/Library/reify_data.ML
--- a/src/HOL/Library/reify_data.ML	Sun Nov 08 16:27:50 2009 +0100
+++ b/src/HOL/Library/reify_data.ML	Sun Nov 08 16:28:18 2009 +0100
@@ -17,12 +17,13 @@
 structure Reify_Data : REIFY_DATA =
 struct
 
-structure Data = GenericDataFun
+structure Data = Generic_Data
 (
   type T = thm list * thm list;
   val empty = ([], []);
   val extend = I;
-  fun merge _ = pairself Thm.merge_thms;
+  fun merge ((ths1, rths1), (ths2, rths2)) =
+    (Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2));
 );
 
 val get = Data.get o Context.Proof;