1.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Mon Dec 07 11:32:12 2015 +0100
1.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Mon Dec 07 14:10:59 2015 +0100
1.3 @@ -18,37 +18,37 @@
1.4 "------------ tests on predicates -------------------------------";
1.5 "------------ tests on predicates -------------------------------";
1.6 "------------ tests on predicates -------------------------------";
1.7 -val t1 = (term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x";
1.8 +val t1 = (Thm.term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x";
1.9 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
1.10 if (term2str t) = "False" then ()
1.11 else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
1.12
1.13 -val t1 = (term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x";
1.14 +val t1 = (Thm.term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x";
1.15 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
1.16 if (term2str t) = "False" then ()
1.17 else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
1.18
1.19 -val t1 = (term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x";
1.20 +val t1 = (Thm.term_of o the o (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 (term2str t) = "False" then ()
1.23 else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
1.24
1.25 -val t1 = (term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
1.26 +val t1 = (Thm.term_of o the o (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 (term2str t) = "True" then ()
1.29 else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
1.30
1.31 -val t1 = (term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
1.32 +val t1 = (Thm.term_of o the o (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 (term2str t) = "True" then ()
1.35 else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
1.36
1.37 -val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
1.38 +val t1 = (Thm.term_of o the o (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 (term2str t) = "True" then ()
1.41 else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
1.42
1.43 -val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
1.44 +val t1 = (Thm.term_of o the o (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 (term2str t) = "True" then ()
1.47 else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";