equal
deleted
inserted
replaced
83 | Abs (_,_,t) => h acc t |
83 | Abs (_,_,t) => h acc t |
84 | _ => acc |
84 | _ => acc |
85 in h [] end; |
85 in h [] end; |
86 in |
86 in |
87 fun is_relevant ctxt ct = |
87 fun is_relevant ctxt ct = |
88 gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt)) |
88 gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt)) |
89 andalso forall (fn Free (_,T) => T = HOLogic.intT) (term_frees (term_of ct)) |
89 andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (term_frees (term_of ct)) |
90 andalso forall (fn Var (_,T) => T = HOLogic.intT) (term_vars (term_of ct)); |
90 andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (term_vars (term_of ct)); |
91 |
91 |
92 fun int_nat_terms ctxt ct = |
92 fun int_nat_terms ctxt ct = |
93 let |
93 let |
94 val cts = snd (CooperData.get ctxt) |
94 val cts = snd (CooperData.get ctxt) |
95 fun h acc t = if ty cts t then insert (op aconvc) t acc else |
95 fun h acc t = if ty cts t then insert (op aconvc) t acc else |