| changeset 33037 | b22e44496dc2 |
| parent 32952 | aeb1e44fbc19 |
| child 33038 | 8f9594c31de4 |
| 33015:575bd6548df9 | 33037:b22e44496dc2 |
|---|---|
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 Logic.all (map Free (frees_in_term ctx t) inter vs') t |
104 fold_rev Logic.all (gen_inter (op =) (map Free (frees_in_term ctx t), vs')) t |
105 end |
105 end |
106 in |
106 in |
107 map instantiate substs |
107 map instantiate substs |
108 end |
108 end |
109 |
109 |