equal
deleted
inserted
replaced
279 val morphism = ProofContext.export_morphism lthy'' lthy |
279 val morphism = ProofContext.export_morphism lthy'' lthy |
280 val fv_frees_exp = map (Morphism.term morphism) fv_frees |
280 val fv_frees_exp = map (Morphism.term morphism) fv_frees |
281 val fv_bns_exp = map (Morphism.term morphism) fv_bns |
281 val fv_bns_exp = map (Morphism.term morphism) fv_bns |
282 |
282 |
283 in |
283 in |
284 ((fv_frees_exp, fv_bns_exp), info, lthy'') |
284 ((fv_frees_exp, fv_bns_exp), @{thms refl}, lthy'') |
285 end |
285 end |
286 *} |
286 *} |
287 |
287 |
288 end |
288 end |