1.1 --- a/test/Tools/isac/Knowledge/poly-1.sml	Wed Aug 03 18:17:27 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/poly-1.sml	Thu Aug 04 12:48:37 2022 +0200
     1.3 @@ -470,7 +470,7 @@
     1.4  
     1.5  "----- eval_is_multUnordered ---";
     1.6  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";
     1.7 -case eval_is_multUnordered "testid" "" tm thy of
     1.8 +case eval_is_multUnordered "testid" "" tm @{context} of
     1.9      SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $ 
    1.10                     (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
    1.11                            (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $ 
    1.12 @@ -492,7 +492,7 @@
    1.13  (*+*)  andalso not (is_multUnordered arg)
    1.14  (*+*)then () else error "sort_variables  3 * a + - 2 * a   CHANGED";
    1.15  
    1.16 -case eval_is_multUnordered "xxx " "yyy " t thy of
    1.17 +case eval_is_multUnordered "xxx " "yyy " t @{context} of
    1.18    SOME
    1.19      ("xxx 3 * a + - 2 * a_",
    1.20        Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
    1.21 @@ -507,7 +507,7 @@
    1.22  (*+*)  andalso not (is_multUnordered arg)
    1.23  (*+*)then () else error "sort_variables  - 2 * a   CHANGED";
    1.24  
    1.25 -case eval_is_multUnordered "xxx " "yyy " t thy of
    1.26 +case eval_is_multUnordered "xxx " "yyy " t @{context} of
    1.27    SOME
    1.28      ("xxx - 2 * a_",
    1.29        Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
    1.30 @@ -521,7 +521,7 @@
    1.31  (*+*)  andalso not (is_multUnordered arg)
    1.32  (*+*)then () else error "sort_variables   a   CHANGED";
    1.33  
    1.34 -case eval_is_multUnordered "xxx " "yyy " t thy of
    1.35 +case eval_is_multUnordered "xxx " "yyy " t @{context} of
    1.36    SOME
    1.37      ("xxx a_",
    1.38        Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
    1.39 @@ -535,7 +535,7 @@
    1.40  (*+*)  andalso not (is_multUnordered arg)
    1.41  (*+*)then () else error "sort_variables   - 2   CHANGED";
    1.42  
    1.43 -case eval_is_multUnordered "xxx " "yyy " t thy of
    1.44 +case eval_is_multUnordered "xxx " "yyy " t @{context} of
    1.45    SOME
    1.46      ("xxx - 2_",
    1.47        Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
    1.48 @@ -676,7 +676,7 @@
    1.49  val t = TermC.str2term "(6 * a) is_multUnordered"; 
    1.50  val SOME
    1.51      (_, t') =
    1.52 -           eval_is_multUnordered "xxx" () t @{theory};
    1.53 +           eval_is_multUnordered "xxx" () t @{context};
    1.54  (*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then () 
    1.55  (*+*)else error "6 * a is_multUnordered = False CHANGED";
    1.56