src/HOL/Library/reify_data.ML
changeset 33518 24563731b9b2
parent 30528 7173bf123335
child 37744 3daaf23b9ab4
     1.1 --- a/src/HOL/Library/reify_data.ML	Sun Nov 08 16:27:50 2009 +0100
     1.2 +++ b/src/HOL/Library/reify_data.ML	Sun Nov 08 16:28:18 2009 +0100
     1.3 @@ -17,12 +17,13 @@
     1.4  structure Reify_Data : REIFY_DATA =
     1.5  struct
     1.6  
     1.7 -structure Data = GenericDataFun
     1.8 +structure Data = Generic_Data
     1.9  (
    1.10    type T = thm list * thm list;
    1.11    val empty = ([], []);
    1.12    val extend = I;
    1.13 -  fun merge _ = pairself Thm.merge_thms;
    1.14 +  fun merge ((ths1, rths1), (ths2, rths2)) =
    1.15 +    (Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2));
    1.16  );
    1.17  
    1.18  val get = Data.get o Context.Proof;