135 (* instantiate *) |
135 (* instantiate *) |
136 |
136 |
137 fun instantiate_frees_morphism ([], []) = identity |
137 fun instantiate_frees_morphism ([], []) = identity |
138 | instantiate_frees_morphism (cinstT, cinst) = |
138 | instantiate_frees_morphism (cinstT, cinst) = |
139 let |
139 let |
140 val instT = map (apsnd Thm.typ_of) cinstT; |
140 val instT = |
141 val inst = map (apsnd Thm.term_of) cinst; |
141 fold (fn (v, cT) => Term_Subst.TFrees.add (v, Thm.typ_of cT)) |
|
142 cinstT Term_Subst.TFrees.empty; |
|
143 val inst = |
|
144 fold (fn (v, ct) => Term_Subst.Frees.add (v, Thm.term_of ct)) |
|
145 cinst Term_Subst.Frees.empty; |
142 in |
146 in |
143 morphism "instantiate_frees" |
147 morphism "instantiate_frees" |
144 {binding = [], |
148 {binding = [], |
145 typ = if null instT then [] else [Term_Subst.instantiateT_frees instT], |
149 typ = |
|
150 if Term_Subst.TFrees.is_empty instT then [] |
|
151 else [Term_Subst.instantiateT_frees instT], |
146 term = [Term_Subst.instantiate_frees (instT, inst)], |
152 term = [Term_Subst.instantiate_frees (instT, inst)], |
147 fact = [map (Thm.instantiate_frees (cinstT, cinst))]} |
153 fact = [map (Thm.instantiate_frees (cinstT, cinst))]} |
148 end; |
154 end; |
149 |
155 |
150 fun instantiate_morphism ([], []) = identity |
156 fun instantiate_morphism ([], []) = identity |
151 | instantiate_morphism (cinstT, cinst) = |
157 | instantiate_morphism (cinstT, cinst) = |
152 let |
158 let |
153 val instT = map (apsnd Thm.typ_of) cinstT; |
159 val instT = |
154 val inst = map (apsnd Thm.term_of) cinst; |
160 fold (fn (v, cT) => Term_Subst.TVars.add (v, Thm.typ_of cT)) |
|
161 cinstT Term_Subst.TVars.empty; |
|
162 val inst = |
|
163 fold (fn (v, ct) => Term_Subst.Vars.add (v, Thm.term_of ct)) |
|
164 cinst Term_Subst.Vars.empty; |
155 in |
165 in |
156 morphism "instantiate" |
166 morphism "instantiate" |
157 {binding = [], |
167 {binding = [], |
158 typ = if null instT then [] else [Term_Subst.instantiateT instT], |
168 typ = |
|
169 if Term_Subst.TVars.is_empty instT then [] |
|
170 else [Term_Subst.instantiateT instT], |
159 term = [Term_Subst.instantiate (instT, inst)], |
171 term = [Term_Subst.instantiate (instT, inst)], |
160 fact = [map (Thm.instantiate (cinstT, cinst))]} |
172 fact = [map (Thm.instantiate (cinstT, cinst))]} |
161 end; |
173 end; |
162 |
174 |
163 end; |
175 end; |