equal
deleted
inserted
replaced
26 fun frees_of t = map Free (rev (Term.add_frees t [])); |
26 fun frees_of t = map Free (rev (Term.add_frees t [])); |
27 |
27 |
28 fun forall_intr_vfs prop = fold_rev Logic.all |
28 fun forall_intr_vfs prop = fold_rev Logic.all |
29 (vars_of prop @ frees_of prop) prop; |
29 (vars_of prop @ frees_of prop) prop; |
30 |
30 |
31 fun forall_intr_prf t prf = |
31 fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof' |
32 let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) |
|
33 in Abst (a, SOME T, prf_abstract_over t prf) end; |
|
34 |
|
35 fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_prf |
|
36 (vars_of prop @ frees_of prop) prf; |
32 (vars_of prop @ frees_of prop) prf; |
37 |
33 |
38 |
34 |
39 (**** generate constraints for proof term ****) |
35 (**** generate constraints for proof term ****) |
40 |
36 |