equal
deleted
inserted
replaced
225 val e_subte = []:term list; |
225 val e_subte = []:term list; |
226 fun subte2str ss = terms2str ss; |
226 fun subte2str ss = terms2str ss; |
227 |
227 |
228 fun subte2sube ss = map term2str ss; |
228 fun subte2sube ss = map term2str ss; |
229 |
229 |
230 (*fun subst2str' thy' (s:subst) = |
|
231 (strs2str o |
|
232 (map (pair2str o |
|
233 (apsnd (Sign.string_of_term (sign_of (assoc_thy thy')))) o |
|
234 (apfst (Sign.string_of_term (sign_of (assoc_thy thy'))))))) s;*) |
|
235 fun subst2subs s = map (pair2str o |
230 fun subst2subs s = map (pair2str o |
236 (apfst (Syntax.string_of_term (thy2ctxt' "Isac"))) o |
231 (apfst (Syntax.string_of_term (thy2ctxt' "Isac"))) o |
237 (apsnd (Syntax.string_of_term (thy2ctxt' "Isac")))) s; |
232 (apsnd (Syntax.string_of_term (thy2ctxt' "Isac")))) s; |
238 fun subst2subs' s = map ((apfst (Syntax.string_of_term (thy2ctxt' "Isac"))) o |
233 fun subst2subs' s = map ((apfst (Syntax.string_of_term (thy2ctxt' "Isac"))) o |
239 (apsnd (Syntax.string_of_term (thy2ctxt' "Isac")))) s; |
234 (apsnd (Syntax.string_of_term (thy2ctxt' "Isac")))) s; |