equal
deleted
inserted
replaced
231 |
231 |
232 val fvbns = map snd bn_fvbn; |
232 val fvbns = map snd bn_fvbn; |
233 val fv_nums = 0 upto (length fv_frees - 1) |
233 val fv_nums = 0 upto (length fv_frees - 1) |
234 |
234 |
235 val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclauses (fv_frees ~~ fv_nums); |
235 val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclauses (fv_frees ~~ fv_nums); |
236 val fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
236 |
237 val fv_eqs_binds = map (fn x => (Attrib.empty_binding, x)) (flat fv_eqs @ flat fv_bn_eqs) |
237 val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
|
238 val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
238 |
239 |
239 val lthy' = |
240 val lthy' = |
240 lthy |
241 lthy |
241 |> Function.add_function fv_names fv_eqs_binds Function_Common.default_config |
242 |> Function.add_function all_fv_names all_fv_eqs Function_Common.default_config |
242 |> by_pat_completeness_auto |
243 |> by_pat_completeness_auto |
243 |> Local_Theory.restore |
244 |> Local_Theory.restore |
244 |> termination_by (Lexicographic_Order.lexicographic_order) |
245 |> termination_by (Lexicographic_Order.lexicographic_order) |
245 in |
246 in |
246 (fv_frees @ fvbns, lthy') |
247 (fv_frees @ fvbns, lthy') |