src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
changeset 74561 8e6c973003c8
parent 73977 2d8a0f8e30ec
equal deleted inserted replaced
74560:5c8177fd1295 74561:8e6c973003c8
   141 
   141 
   142 structure Data = Theory_Data
   142 structure Data = Theory_Data
   143 (
   143 (
   144   type T = lfp_rec_extension option;
   144   type T = lfp_rec_extension option;
   145   val empty = NONE;
   145   val empty = NONE;
   146   val extend = I;
       
   147   val merge = merge_options;
   146   val merge = merge_options;
   148 );
   147 );
   149 
   148 
   150 val register_lfp_rec_extension = Data.put o SOME;
   149 val register_lfp_rec_extension = Data.put o SOME;
   151 
   150