src/HOL/Tools/Nitpick/nitpick_isar.ML
changeset 33699 f33b036ef318
parent 33604 d4220df6fde2
child 33982 1ae222745c4a
equal deleted inserted replaced
33698:b5f36fa5a7b4 33699:f33b036ef318
   135 structure Data = Theory_Data(
   135 structure Data = Theory_Data(
   136   type T = {params: raw_param list}
   136   type T = {params: raw_param list}
   137   val empty = {params = rev default_default_params}
   137   val empty = {params = rev default_default_params}
   138   val extend = I
   138   val extend = I
   139   fun merge ({params = ps1}, {params = ps2}) : T =
   139   fun merge ({params = ps1}, {params = ps2}) : T =
   140     {params = AList.merge (op =) (op =) (ps1, ps2)})
   140     {params = AList.merge (op =) (K true) (ps1, ps2)})
   141 
   141 
   142 (* raw_param -> theory -> theory *)
   142 (* raw_param -> theory -> theory *)
   143 fun set_default_raw_param param thy =
   143 fun set_default_raw_param param thy =
   144   let val {params} = Data.get thy in
   144   let val {params} = Data.get thy in
   145     Data.put {params = AList.update (op =) (unnegate_raw_param param) params}
   145     Data.put {params = AList.update (op =) (unnegate_raw_param param) params}