1.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_2.thy	Tue Jan 31 11:23:16 2023 +0100
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_2.thy	Tue Jan 31 12:29:42 2023 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4    @{term "\<delta> "};
     1.5    @{term "\<phi> "};
     1.6    @{term "\<rho> "};
     1.7 -  UnparseC.term @{term "\<rho> "};
     1.8 +  UnparseC.term_in_ctxt @{context} @{term "\<rho> "};
     1.9  \<close>
    1.10  
    1.11  section\<open>Working with Rulesets\<close>
    1.12 @@ -48,9 +48,9 @@
    1.13  \<close>
    1.14  
    1.15  ML\<open>
    1.16 - UnparseC.term t';
    1.17 - UnparseC.term t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
    1.18 - UnparseC.term t' = "?u [?n] + \<alpha>\<up>?n u[n] + ?\<delta> [?n]";
    1.19 + UnparseC.term_in_ctxt @{context} t';
    1.20 + UnparseC.term_in_ctxt @{context} t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
    1.21 + UnparseC.term_in_ctxt @{context} t' = "?u [?n] + \<alpha>\<up>?n u[n] + ?\<delta> [?n]";
    1.22  \<close>
    1.23  
    1.24  text\<open>Problems: Rule~1 is applied before the expression is checked for Rule~4