diff -r 0d22a6bf1fc6 -r 0ee698b0a703 test/Tools/isac/Knowledge/poly-1.sml
--- a/test/Tools/isac/Knowledge/poly-1.sml	Tue Jul 20 14:37:56 2021 +0200
+++ b/test/Tools/isac/Knowledge/poly-1.sml	Tue Jul 27 11:21:14 2021 +0200
@@ -45,135 +45,135 @@
 "-------- fun has_degree_in --------------------------------------------------------------------";
 "-------- fun has_degree_in --------------------------------------------------------------------";
 "-------- fun has_degree_in --------------------------------------------------------------------";
-val v = TermC.parseNEW'' thy "x";
-val t = TermC.parseNEW'' thy "1";
+val v = (Thm.term_of o the o (TermC.parse thy)) "x";
+val t = (Thm.term_of o the o (TermC.parse thy)) "1";
 if has_degree_in t v = 0 then () else error "has_degree_in (1) x";
 
-val v = TermC.parseNEW'' thy "AA";
-val t = TermC.parseNEW'' thy "1";
+val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
+val t = (Thm.term_of o the o (TermC.parse thy)) "1";
 if has_degree_in t v = 0 then () else error "has_degree_in (1) AA";
 
 (*----------*)
-val v = TermC.parseNEW'' thy "x";
-val t = TermC.parseNEW'' thy "a*b+c";
+val v = (Thm.term_of o the o (TermC.parse thy)) "x";
+val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x";
 
-val v = TermC.parseNEW'' thy "AA";
-val t = TermC.parseNEW'' thy "a*b+c";
+val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
+val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA";
 
 (*----------*)
-val v = TermC.parseNEW'' thy "x";
-val t = TermC.parseNEW'' thy "a*x+c";
+val v = (Thm.term_of o the o (TermC.parse thy)) "x";
+val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c";
 if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x";
 
-val v = TermC.parseNEW'' thy "AA";
-val t = TermC.parseNEW'' thy "a*AA+c";
+val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
+val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c";
 if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA";
 
 (*----------*)
-val v = TermC.parseNEW'' thy "x";
-val t = TermC.parseNEW'' thy "(a*b+c)*x \<up> 7";
+val v = (Thm.term_of o the o (TermC.parse thy)) "x";
+val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x \<up> 7) x";
 
-val v = TermC.parseNEW'' thy "AA";
-val t = TermC.parseNEW'' thy "(a*b+c)*AA \<up> 7";
+val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
+val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA \<up> 7) AA";
 
 (*----------*)
-val v = TermC.parseNEW'' thy "x";
-val t = TermC.parseNEW'' thy "x \<up> 7";
+val v = (Thm.term_of o the o (TermC.parse thy)) "x";
+val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
 if has_degree_in t v = 7 then () else error "has_degree_in (x \<up> 7) x";
 
-val v = TermC.parseNEW'' thy "AA";
-val t = TermC.parseNEW'' thy "AA \<up> 7";
+val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
+val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
 if has_degree_in t v = 7 then () else error "has_degree_in (AA \<up> 7) AA";
 
 (*----------*)
-val v = TermC.parseNEW'' thy "x";
-val t = TermC.parseNEW'' thy "(a*b+c)*x";
+val v = (Thm.term_of o the o (TermC.parse thy)) "x";
+val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x";
 
-val v = TermC.parseNEW'' thy "AA";
-val t = TermC.parseNEW'' thy "(a*b+c)*AA";
+val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
+val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA";
 
 (*----------*)
-val v = TermC.parseNEW'' thy "x";
-val t = TermC.parseNEW'' thy "(a*b+x)*x";
+val v = (Thm.term_of o the o (TermC.parse thy)) "x";
+val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
 if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x";
 
-val v = TermC.parseNEW'' thy "AA";
-val t = TermC.parseNEW'' thy "(a*b+AA)*AA";
+val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
+val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
 if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA";
 
 (*----------*)
-val v = TermC.parseNEW'' thy "x";
-val t = TermC.parseNEW'' thy "x";
+val v = (Thm.term_of o the o (TermC.parse thy)) "x";
+val t = (Thm.term_of o the o (TermC.parse thy)) "x";
 if has_degree_in t v = 1 then () else error "has_degree_in (x) x";
 
-val v = TermC.parseNEW'' thy "AA";
-val t = TermC.parseNEW'' thy "AA";
+val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
+val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
 if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA";
 
 (*----------*)
-val v = TermC.parseNEW'' thy "x";
-val t = TermC.parseNEW'' thy "ab - (a*b)*x";
+val v = (Thm.term_of o the o (TermC.parse thy)) "x";
+val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x";
 
-val v = TermC.parseNEW'' thy "AA";
-val t = TermC.parseNEW'' thy "ab - (a*b)*AA";
+val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
+val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA";
 
 "-------- fun mono_deg_in ----------------------------------------------------------------------";
 "-------- fun mono_deg_in ----------------------------------------------------------------------";
 "-------- fun mono_deg_in ----------------------------------------------------------------------";
-val v = TermC.parseNEW'' thy "x";
+val v = (Thm.term_of o the o (TermC.parse thy)) "x";
 
-val t = TermC.parseNEW'' thy "(a*b+c)*x \<up> 7";
+val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x \<up> 7) x changed";
 
-val t = TermC.parseNEW'' thy "x \<up> 7";
+val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x \<up> 7) x changed";
 
-val t = TermC.parseNEW'' thy "(a*b+c)*x";
+val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed";
 
-val t = TermC.parseNEW'' thy "(a*b+x)*x";
+val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed";
 
-val t = TermC.parseNEW'' thy "x";
+val t = (Thm.term_of o the o (TermC.parse thy)) "x";
 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed";
 
-val t = TermC.parseNEW'' thy "(a*b+c)";
+val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed";
 
-val t = TermC.parseNEW'' thy "ab - (a*b)*x";
+val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";
 
 (*. . . . . . . . . . . . the same with Const (\<^const_name>\<open>AA\<close>, _) . . . . . . . . . . . *)
 val thy = @{theory Partial_Fractions}
-val v = TermC.parseNEW'' thy "AA";
+val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
 
-val t = TermC.parseNEW'' thy "(a*b+c)*AA \<up> 7";
+val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA \<up> 7) AA changed";
 
-val t = TermC.parseNEW'' thy "AA \<up> 7";
+val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA \<up> 7) AA changed";
 
-val t = TermC.parseNEW'' thy "(a*b+c)*AA";
+val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed";
 
-val t = TermC.parseNEW'' thy "(a*b+AA)*AA";
+val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed";
 
-val t = TermC.parseNEW'' thy "AA";
+val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed";
 
-val t = TermC.parseNEW'' thy "(a*b+c)";
+val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed";
 
-val t = TermC.parseNEW'' thy "ab - (a*b)*AA";
+val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed";
 
 
@@ -787,7 +787,7 @@
 else error "poly.sml: diff.behav. in make_polynomial 20";
 
 "-----SPO ---";
-val t = TermC.parseNEW'' thy "a \<up> 2 * (-a) \<up> 2";
+val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * (-a) \<up> 2";
 val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
 if (UnparseC.term t) = "a \<up> 4" then ()
 else error "poly.sml: diff.behav. in make_polynomial 24";