1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Mon Dec 07 11:32:12 2015 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Mon Dec 07 14:10:59 2015 +0100
     1.3 @@ -238,7 +238,7 @@
     1.4  \  (((Try (Rewrite_Set ordne_alphabetisch False)) @@     \
     1.5  \    (Try (Rewrite_Set fasse_zusammen False)) @@     \
     1.6  \    (Try (Rewrite_Set verschoenere False))) t_t)"
     1.7 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
     1.8 +val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
     1.9  atomty sc;
    1.10  
    1.11  "----------- me simplification.for_polynomials.with_minus";
    1.12 @@ -344,7 +344,7 @@
    1.13  \ in (Repeat((Try (Repeat (Calculate TIMES))) @@  \
    1.14  \            (Try (Repeat (Calculate PLUS ))) @@  \
    1.15  \            (Try (Repeat (Calculate MINUS))))) e_e)"
    1.16 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.17 +val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
    1.18  atomty sc;
    1.19  
    1.20  "----------- pbl polynom probe -----------------------------------";