equal
deleted
inserted
replaced
238 |
238 |
239 val {fs, simps, inducts, ...} = info; |
239 val {fs, simps, inducts, ...} = info; |
240 |
240 |
241 val morphism = ProofContext.export_morphism lthy'' lthy |
241 val morphism = ProofContext.export_morphism lthy'' lthy |
242 val fs_exp = map (Morphism.term morphism) fs |
242 val fs_exp = map (Morphism.term morphism) fs |
243 |
243 val simps_exp = map (Morphism.thm morphism) (the simps) |
|
244 val inducts_exp = map (Morphism.thm morphism) (the inducts) |
244 val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp |
245 val (fv_frees_exp, fv_bns_exp) = chop (length fv_frees) fs_exp |
245 val simps_exp = map (Morphism.thm morphism) (the simps) |
246 |
246 val fv_bns_inducts_exp = map (Morphism.thm morphism) (the inducts) |
247 in |
247 in |
248 (fv_frees_exp, fv_bns_exp, simps_exp, inducts_exp, lthy'') |
248 (fv_frees_exp, fv_bns_exp, simps_exp, fv_bns_inducts_exp, lthy'') |
|
249 end |
249 end |
250 |
250 |
251 |
251 |
252 (** equivarance proofs **) |
252 (** equivarance proofs **) |
253 |
253 |