29 fun forall_intr (t, prop) = |
29 fun forall_intr (t, prop) = |
30 let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) |
30 let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) |
31 in all T $ Abs (a, T, abstract_over (t, prop)) end; |
31 in all T $ Abs (a, T, abstract_over (t, prop)) end; |
32 |
32 |
33 fun forall_intr_vfs prop = foldr forall_intr prop |
33 fun forall_intr_vfs prop = foldr forall_intr prop |
34 (vars_of prop @ sort (make_ord atless) (term_frees prop)); |
34 (vars_of prop @ sort Term.term_ord (term_frees prop)); |
35 |
35 |
36 fun forall_intr_prf (t, prf) = |
36 fun forall_intr_prf (t, prf) = |
37 let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) |
37 let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) |
38 in Abst (a, SOME T, prf_abstract_over t prf) end; |
38 in Abst (a, SOME T, prf_abstract_over t prf) end; |
39 |
39 |
40 fun forall_intr_vfs_prf prop prf = foldr forall_intr_prf prf |
40 fun forall_intr_vfs_prf prop prf = foldr forall_intr_prf prf |
41 (vars_of prop @ sort (make_ord atless) (term_frees prop)); |
41 (vars_of prop @ sort Term.term_ord (term_frees prop)); |
42 |
42 |
43 fun merge_envs (Envir.Envir {asol=asol1, iTs=iTs1, maxidx=maxidx1}) |
43 fun merge_envs (Envir.Envir {asol=asol1, iTs=iTs1, maxidx=maxidx1}) |
44 (Envir.Envir {asol=asol2, iTs=iTs2, maxidx=maxidx2}) = |
44 (Envir.Envir {asol=asol2, iTs=iTs2, maxidx=maxidx2}) = |
45 Envir.Envir {asol=Vartab.merge (op =) (asol1, asol2), |
45 Envir.Envir {asol=Vartab.merge (op =) (asol1, asol2), |
46 iTs=Vartab.merge (op =) (iTs1, iTs2), |
46 iTs=Vartab.merge (op =) (iTs1, iTs2), |