src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 33522 737589bb9bb8
parent 33351 37ec56ac3fd4
child 33583 b5e0909cd5ea
equal deleted inserted replaced
33521:a4c54218be62 33522:737589bb9bb8
   177   skolems: (string * string list) list Unsynchronized.ref,
   177   skolems: (string * string list) list Unsynchronized.ref,
   178   special_funs: special_fun list Unsynchronized.ref,
   178   special_funs: special_fun list Unsynchronized.ref,
   179   unrolled_preds: unrolled list Unsynchronized.ref,
   179   unrolled_preds: unrolled list Unsynchronized.ref,
   180   wf_cache: wf_cache Unsynchronized.ref}
   180   wf_cache: wf_cache Unsynchronized.ref}
   181 
   181 
   182 structure TheoryData = TheoryDataFun(
   182 structure TheoryData = Theory_Data(
   183   type T = {frac_types: (string * (string * string) list) list,
   183   type T = {frac_types: (string * (string * string) list) list,
   184             codatatypes: (string * (string * styp list)) list}
   184             codatatypes: (string * (string * styp list)) list}
   185   val empty = {frac_types = [], codatatypes = []}
   185   val empty = {frac_types = [], codatatypes = []}
   186   val copy = I
       
   187   val extend = I
   186   val extend = I
   188   fun merge _ ({frac_types = fs1, codatatypes = cs1},
   187   fun merge ({frac_types = fs1, codatatypes = cs1},
   189                {frac_types = fs2, codatatypes = cs2}) =
   188                {frac_types = fs2, codatatypes = cs2}) : T =
   190     {frac_types = AList.merge (op =) (op =) (fs1, fs2),
   189     {frac_types = AList.merge (op =) (op =) (fs1, fs2),
   191      codatatypes = AList.merge (op =) (op =) (cs1, cs2)})
   190      codatatypes = AList.merge (op =) (op =) (cs1, cs2)})
   192 
   191 
   193 (* term * term -> term *)
   192 (* term * term -> term *)
   194 fun s_conj (t1, @{const True}) = t1
   193 fun s_conj (t1, @{const True}) = t1