| changeset 27330 | 1af2598b5f7d |
| parent 25538 | 58e8ba3b792b |
| child 31723 | f5cafe803b55 |
| 27329:91c0c894e1b4 | 27330:1af2598b5f7d |
|---|---|
99 |
99 |
100 fun instantiate (vs', sigma) = |
100 fun instantiate (vs', sigma) = |
101 let |
101 let |
102 val t = Pattern.rewrite_term thy sigma [] feq1 |
102 val t = Pattern.rewrite_term thy sigma [] feq1 |
103 in |
103 in |
104 fold_rev mk_forall (map Free (frees_in_term ctx t) inter vs') t |
104 fold_rev Logic.all (map Free (frees_in_term ctx t) inter vs') t |
105 end |
105 end |
106 in |
106 in |
107 map instantiate substs |
107 map instantiate substs |
108 end |
108 end |
109 |
109 |