equal
deleted
inserted
replaced
263 val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn_map) bclausesss (fv_frees ~~ fv_nums); |
263 val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn_map) bclausesss (fv_frees ~~ fv_nums); |
264 |
264 |
265 val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
265 val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
266 val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
266 val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
267 |
267 |
|
268 val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) (flat fv_bn_eqs))) |
|
269 |
268 fun pat_completeness_auto ctxt = |
270 fun pat_completeness_auto ctxt = |
269 Pat_Completeness.pat_completeness_tac ctxt 1 |
271 Pat_Completeness.pat_completeness_tac ctxt 1 |
270 THEN auto_tac (clasimpset_of ctxt) |
272 THEN auto_tac (clasimpset_of ctxt) |
271 |
273 |
272 fun prove_termination lthy = |
274 fun prove_termination lthy = |