src/HOL/Tools/Qelim/langford_data.ML

--- a/src/HOL/Tools/Qelim/langford_data.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/Qelim/langford_data.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -17,12 +17,13 @@
 val eq_key = Thm.eq_thm;
 fun eq_data arg = eq_fst eq_key arg;
 
-structure Data = GenericDataFun
-( type T = simpset * (thm * entry) list;
+structure Data = Generic_Data
+(
+  type T = simpset * (thm * entry) list;
   val empty = (HOL_basic_ss, []);
   val extend = I;
-  fun merge _ ((ss1,es1), (ss2,es2)) = 
-       (merge_ss (ss1,ss2), AList.merge eq_key (K true) (es1,es2));;
+  fun merge ((ss1, es1), (ss2, es2)) : T =
+    (merge_ss (ss1, ss2), AList.merge eq_key (K true) (es1, es2));
 );
 
 val get = Data.get o Context.Proof;