adapted Generic_Data;
authorwenzelm
Sun Nov 08 16:28:18 2009 +0100 (2009-11-08)
changeset 3351824563731b9b2
parent 33517 d064fa48f305
child 33519 e31a85f92ce9
adapted Generic_Data;
proper merge of fst/fst and snd/snd;
src/HOL/Library/reify_data.ML
     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;