279 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
279 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
280 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
280 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
281 |
281 |
282 val (info, lthy'') = prove_termination_fun size_simps (Local_Theory.restore lthy') |
282 val (info, lthy'') = prove_termination_fun size_simps (Local_Theory.restore lthy') |
283 |
283 |
284 val {fs, simps, inducts, ...} = info; |
284 val {fs, simps, inducts, ...} = info; |
285 |
285 |
286 val morphism = ProofContext.export_morphism lthy'' lthy |
286 val morphism = ProofContext.export_morphism lthy'' lthy |
287 val simps_exp = map (Morphism.thm morphism) (the simps) |
287 val simps_exp = map (Morphism.thm morphism) (the simps) |
288 val inducts_exp = map (Morphism.thm morphism) (the inducts) |
288 val inducts_exp = map (Morphism.thm morphism) (the inducts) |
289 |
289 |
290 val (fvs', fv_bns') = chop (length fv_frees) fs |
290 val (fvs', fv_bns') = chop (length fv_frees) fs |
291 in |
291 |
292 (fvs', fv_bns', simps_exp, inducts_exp, lthy'') |
292 (* grafting the types so that they coincide with the input into the function package *) |
|
293 val fvs'' = map2 (fn t => fn ty => Const (fst (dest_Const t), ty) ) fvs' fv_tys |
|
294 val fv_bns'' = map2 (fn t => fn ty => Const (fst (dest_Const t), ty) ) fv_bns' fv_bn_tys |
|
295 in |
|
296 (fvs'', fv_bns'', simps_exp, inducts_exp, lthy'') |
293 end |
297 end |
294 |
298 |
295 |
299 |
296 (** definition of raw permute_bn functions **) |
300 (** definition of raw permute_bn functions **) |
297 |
301 |