equal
deleted
inserted
replaced
188 | chk_prepat thy erls prepat t = |
188 | chk_prepat thy erls prepat t = |
189 let fun chk (pres, pat) = |
189 let fun chk (pres, pat) = |
190 (let val subst: Type.tyenv * Envir.tenv = |
190 (let val subst: Type.tyenv * Envir.tenv = |
191 Pattern.match thy (pat, t) |
191 Pattern.match thy (pat, t) |
192 (Vartab.empty, Vartab.empty) |
192 (Vartab.empty, Vartab.empty) |
193 val _ = tracing ("app_rev: pres=------------------"); |
|
194 val _ = tracing ("app_rev: pres=" ^ terms2str pres); |
|
195 val _ = tracing ("app_rev: pat =" ^ term2str pat); |
|
196 val _ = tracing ("app_rev: t =" ^ term2str t); |
|
197 in snd (eval__true thy (i+1) |
193 in snd (eval__true thy (i+1) |
198 (map (Envir.subst_term subst) pres) |
194 (map (Envir.subst_term subst) pres) |
199 [] erls) |
195 [] erls) |
200 end) |
196 end) |
201 handle _ => false |
197 handle _ => false |