equal
deleted
inserted
replaced
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 (inter (op =) (map Free (frees_in_term ctx t), vs')) t |
104 fold_rev Logic.all (inter (op =) vs' (map Free (frees_in_term ctx t))) t |
105 end |
105 end |
106 in |
106 in |
107 map instantiate substs |
107 map instantiate substs |
108 end |
108 end |
109 |
109 |