1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Tue May 24 16:47:31 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Thu May 26 12:44:51 2022 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4  "--------------------------------------------------------";
     1.5  
     1.6  val thy = @{theory "PolyMinus"};
     1.7 +val ctxt = Proof_Context.init_global thy;
     1.8  
     1.9  "----------- fun identifier --------------------------------------------------------------------";
    1.10  "----------- fun identifier --------------------------------------------------------------------";
    1.11 @@ -341,7 +342,7 @@
    1.12  \  (((Try (Rewrite_Set ordne_alphabetisch False)) #>     \
    1.13  \    (Try (Rewrite_Set fasse_zusammen False)) #>     \
    1.14  \    (Try (Rewrite_Set verschoenere False))) t_t)"
    1.15 -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
    1.16 +val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
    1.17  TermC.atomty sc;
    1.18  
    1.19  "----------- me simplification.for_polynomials.with_minus";
    1.20 @@ -448,7 +449,7 @@
    1.21  \ in (Repeat((Try (Repeat (Calculate ''TIMES''))) #>  \
    1.22  \            (Try (Repeat (Calculate ''PLUS''))) #>  \
    1.23  \            (Try (Repeat (Calculate ''MINUS''))))) e_e)"
    1.24 -val sc = (inst_abs o Thm.term_of o the o (TermC.parse thy)) str;
    1.25 +val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
    1.26  TermC.atomty sc;
    1.27  
    1.28  "----------- pbl polynom probe -----------------------------------";