equal
deleted
inserted
replaced
269 (fold Term.maxidx_term ts ~1 + 1)) ts; |
269 (fold Term.maxidx_term ts ~1 + 1)) ts; |
270 |
270 |
271 fun gen_export inst inner outer ths = |
271 fun gen_export inst inner outer ths = |
272 let |
272 let |
273 val ths' = map Thm.adjust_maxidx_thm ths; |
273 val ths' = map Thm.adjust_maxidx_thm ths; |
274 val maxidx = fold Thm.maxidx_thm ths' ~1; |
|
275 val inner' = fold (declare_occs o Thm.full_prop_of) ths' inner; |
274 val inner' = fold (declare_occs o Thm.full_prop_of) ths' inner; |
276 in map (Thm.generalize (inst inner' outer) (maxidx + 1)) ths' end; |
275 in map (Thm.generalize (inst inner' outer) (fold Thm.maxidx_thm ths' ~1 + 1)) ths' end; |
277 |
276 |
278 val exportT = gen_export (rpair [] oo exportT_inst); |
277 val exportT = gen_export (rpair [] oo exportT_inst); |
279 val export = gen_export export_inst; |
278 val export = gen_export export_inst; |
280 |
279 |
281 |
280 |
366 |
365 |
367 fun monomorphic ctxt ts = |
366 fun monomorphic ctxt ts = |
368 #1 (importT_terms ts (fold declare_term ts ctxt)); |
367 #1 (importT_terms ts (fold declare_term ts ctxt)); |
369 |
368 |
370 fun polymorphic ctxt ts = |
369 fun polymorphic ctxt ts = |
371 exportT_terms (fold declare_term ts ctxt) ctxt ts; |
370 let |
|
371 val ctxt' = fold declare_term ts ctxt; |
|
372 val types = subtract (op =) (used_types ctxt) (used_types ctxt'); |
|
373 val idx = fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1; |
|
374 in map (Term.generalize (types, []) idx) ts end; |
|
375 |
372 |
376 |
373 |
377 |
374 (** term bindings **) |
378 (** term bindings **) |
375 |
379 |
376 fun hidden_polymorphism t T = |
380 fun hidden_polymorphism t T = |