1.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml	Tue Jul 20 14:37:56 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml	Tue Jul 27 11:21:14 2021 +0200
     1.3 @@ -27,37 +27,37 @@
     1.4  "------------ tests on predicates  -------------------------------";
     1.5  "------------ tests on predicates  -------------------------------";
     1.6  "------------ tests on predicates  -------------------------------";
     1.7 -val t1 = TermC.parseNEW'' thy "(-8 - sqrt(x) + x \<up> 2) is_rootRatAddTerm_in x";
     1.8 +val t1 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - sqrt(x) + x \<up> 2) is_rootRatAddTerm_in x";
     1.9  val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
    1.10  if (UnparseC.term t) = "False" then ()
    1.11   else  error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
    1.12  
    1.13 -val t1 = TermC.parseNEW'' thy "(1/x) is_rootRatAddTerm_in x";
    1.14 +val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/x) is_rootRatAddTerm_in x";
    1.15  val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
    1.16  if (UnparseC.term t) = "False" then ()
    1.17   else  error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
    1.18  
    1.19 -val t1 = TermC.parseNEW'' thy "(1/sqrt(x)) is_rootRatAddTerm_in x";
    1.20 +val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x";
    1.21  val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
    1.22  if (UnparseC.term t) = "False" then ()
    1.23   else  error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
    1.24  
    1.25 -val t1 = TermC.parseNEW'' thy "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
    1.26 +val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
    1.27  val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
    1.28  if (UnparseC.term t) = "True" then ()
    1.29   else  error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
    1.30  
    1.31 -val t1 = TermC.parseNEW'' thy "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
    1.32 +val t1 = (Thm.term_of o the o (TermC.parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
    1.33  val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
    1.34  if (UnparseC.term t) = "True" then ()
    1.35   else  error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
    1.36  
    1.37 -val t1 = TermC.parseNEW'' thy "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
    1.38 +val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
    1.39  val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
    1.40  if (UnparseC.term t) = "True" then ()
    1.41   else  error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
    1.42  
    1.43 -val t1 = TermC.parseNEW'' thy "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
    1.44 +val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
    1.45  val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
    1.46  if (UnparseC.term t) = "True" then ()
    1.47   else  error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";