src/HOL/Library/reify_data.ML
changeset 33518 24563731b9b2
parent 30528 7173bf123335
child 37744 3daaf23b9ab4
equal deleted inserted replaced
33517:d064fa48f305 33518:24563731b9b2
    15 end;
    15 end;
    16 
    16 
    17 structure Reify_Data : REIFY_DATA =
    17 structure Reify_Data : REIFY_DATA =
    18 struct
    18 struct
    19 
    19 
    20 structure Data = GenericDataFun
    20 structure Data = Generic_Data
    21 (
    21 (
    22   type T = thm list * thm list;
    22   type T = thm list * thm list;
    23   val empty = ([], []);
    23   val empty = ([], []);
    24   val extend = I;
    24   val extend = I;
    25   fun merge _ = pairself Thm.merge_thms;
    25   fun merge ((ths1, rths1), (ths2, rths2)) =
       
    26     (Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2));
    26 );
    27 );
    27 
    28 
    28 val get = Data.get o Context.Proof;
    29 val get = Data.get o Context.Proof;
    29 
    30 
    30 val add = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);
    31 val add = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);