test/Tools/isac/Knowledge/algein.sml
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