1.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml	Tue May 24 16:47:31 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml	Thu May 26 12:44:51 2022 +0200
     1.3 @@ -21,43 +21,44 @@
     1.4  (a) either method ["RootEq", "solve_sq_root_equation"] & Co are somewhat indeterministic
     1.5  (b) of this is a case of indeterminism due to something elementary.
     1.6  
     1.7 -*)
     1.8 +*)                               
     1.9  val thy = @{theory "RootRatEq"};
    1.10 +val ctxt = Proof_Context.init_global thy;
    1.11  
    1.12  "------------ tests on predicates  -------------------------------";
    1.13  "------------ tests on predicates  -------------------------------";
    1.14  "------------ tests on predicates  -------------------------------";
    1.15 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - sqrt(x) + x \<up> 2) is_rootRatAddTerm_in x";
    1.16 +val t1 = TermC.parseNEW' ctxt "(-8 - sqrt(x) + x \<up> 2) is_rootRatAddTerm_in x";
    1.17  val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
    1.18  if (UnparseC.term t) = "False" then ()
    1.19   else  error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
    1.20  
    1.21 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/x) is_rootRatAddTerm_in x";
    1.22 +val t1 = TermC.parseNEW' ctxt "(1/x) is_rootRatAddTerm_in x";
    1.23  val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
    1.24  if (UnparseC.term t) = "False" then ()
    1.25   else  error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
    1.26  
    1.27 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x";
    1.28 +val t1 = TermC.parseNEW' ctxt "(1/sqrt(x)) is_rootRatAddTerm_in x";
    1.29  val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
    1.30  if (UnparseC.term t) = "False" then ()
    1.31   else  error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
    1.32  
    1.33 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
    1.34 +val t1 = TermC.parseNEW' ctxt "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
    1.35  val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
    1.36  if (UnparseC.term t) = "True" then ()
    1.37   else  error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
    1.38  
    1.39 -val t1 = (Thm.term_of o the o (TermC.parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
    1.40 +val t1 = TermC.parseNEW' ctxt "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
    1.41  val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
    1.42  if (UnparseC.term t) = "True" then ()
    1.43   else  error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
    1.44  
    1.45 -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.46 +val t1 = TermC.parseNEW' ctxt "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
    1.47  val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
    1.48  if (UnparseC.term t) = "True" then ()
    1.49   else  error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
    1.50  
    1.51 -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.52 +val t1 = TermC.parseNEW' ctxt "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
    1.53  val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
    1.54  if (UnparseC.term t) = "True" then ()
    1.55   else  error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";