diff -r ce09935439b3 -r 2e0b7ca391dc test/Tools/isac/Knowledge/poly-1.sml
--- a/test/Tools/isac/Knowledge/poly-1.sml	Wed Aug 03 18:17:27 2022 +0200
+++ b/test/Tools/isac/Knowledge/poly-1.sml	Thu Aug 04 12:48:37 2022 +0200
@@ -470,7 +470,7 @@
 
 "----- eval_is_multUnordered ---";
 val tm = TermC.str2term "(5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (- 1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + - 1 * (3 * x \<up> 5 * - 1) +  (-48 * x \<up> 4 + 8))) is_multUnordered";
-case eval_is_multUnordered "testid" "" tm thy of
+case eval_is_multUnordered "testid" "" tm @{context} of
     SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $ 
                    (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
                           (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $ 
@@ -492,7 +492,7 @@
 (*+*)  andalso not (is_multUnordered arg)
 (*+*)then () else error "sort_variables  3 * a + - 2 * a   CHANGED";
 
-case eval_is_multUnordered "xxx " "yyy " t thy of
+case eval_is_multUnordered "xxx " "yyy " t @{context} of
   SOME
     ("xxx 3 * a + - 2 * a_",
       Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
@@ -507,7 +507,7 @@
 (*+*)  andalso not (is_multUnordered arg)
 (*+*)then () else error "sort_variables  - 2 * a   CHANGED";
 
-case eval_is_multUnordered "xxx " "yyy " t thy of
+case eval_is_multUnordered "xxx " "yyy " t @{context} of
   SOME
     ("xxx - 2 * a_",
       Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
@@ -521,7 +521,7 @@
 (*+*)  andalso not (is_multUnordered arg)
 (*+*)then () else error "sort_variables   a   CHANGED";
 
-case eval_is_multUnordered "xxx " "yyy " t thy of
+case eval_is_multUnordered "xxx " "yyy " t @{context} of
   SOME
     ("xxx a_",
       Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
@@ -535,7 +535,7 @@
 (*+*)  andalso not (is_multUnordered arg)
 (*+*)then () else error "sort_variables   - 2   CHANGED";
 
-case eval_is_multUnordered "xxx " "yyy " t thy of
+case eval_is_multUnordered "xxx " "yyy " t @{context} of
   SOME
     ("xxx - 2_",
       Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
@@ -676,7 +676,7 @@
 val t = TermC.str2term "(6 * a) is_multUnordered"; 
 val SOME
     (_, t') =
-           eval_is_multUnordered "xxx" () t @{theory};
+           eval_is_multUnordered "xxx" () t @{context};
 (*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then () 
 (*+*)else error "6 * a is_multUnordered = False CHANGED";