equal
deleted
inserted
replaced
152 then () else error "update_ptyps has changed 3"; |
152 then () else error "update_ptyps has changed 3"; |
153 |
153 |
154 "----------- fun subst2str' --------------------------------------------------------------------"; |
154 "----------- fun subst2str' --------------------------------------------------------------------"; |
155 "----------- fun subst2str' --------------------------------------------------------------------"; |
155 "----------- fun subst2str' --------------------------------------------------------------------"; |
156 "----------- fun subst2str' --------------------------------------------------------------------"; |
156 "----------- fun subst2str' --------------------------------------------------------------------"; |
157 (*> subst2str' [(TermC.str2term "bdv", TermC.str2term "x"), |
157 (*> subst2str' [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x"), |
158 (TermC.str2term "bdv_2", TermC.str2term "y")]; |
158 (TermC.parse_test @{context} "bdv_2", TermC.parse_test @{context} "y")]; |
159 val it = "[(bdv, x)]" : string |
159 val it = "[(bdv, x)]" : string |
160 *) |
160 *) |