1.1 --- a/test/Tools/isac/Knowledge/algein.sml	Tue May 24 16:47:31 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Thu May 26 12:44:51 2022 +0200
     1.3 @@ -15,10 +15,7 @@
     1.4  "-----------------------------------------------------------------";
     1.5  
     1.6  val thy = @{theory "AlgEin"};
     1.7 -
     1.8 -
     1.9 -(* use"../smltest/IsacKnowledge/algein.sml";
    1.10 -   *)
    1.11 +val ctxt = Proof_Context.init_global thy;
    1.12  
    1.13  "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
    1.14  "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
    1.15 @@ -29,7 +26,7 @@
    1.16  \ (let t_t = (l_l = 1)\
    1.17  \ in t_t)"
    1.18  ;
    1.19 -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
    1.20 +val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
    1.21  TermC.atomty sc;
    1.22  atomt sc;
    1.23