changeset 60339 | 0d22a6bf1fc6 |
parent 60230 | 0ca0f9363ad3 |
child 60340 | 0ee698b0a703 |
1.1 --- a/test/Tools/isac/Knowledge/algein.sml Mon Jul 19 18:39:02 2021 +0200 1.2 +++ b/test/Tools/isac/Knowledge/algein.sml Tue Jul 20 14:37:56 2021 +0200 1.3 @@ -29,7 +29,7 @@ 1.4 \ (let t_t = (l_l = 1)\ 1.5 \ in t_t)" 1.6 ; 1.7 -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str; 1.8 +val sc = (inst_abs o (TermC.parseNEW'' thy)) str; 1.9 TermC.atomty sc; 1.10 atomt sc; 1.11