test/Tools/isac/MathEngine/step.sml
changeset 60675 d841c720d288
parent 60665 fad0cbfb586d
child 60739 78a78f428ef8
     1.1 --- a/test/Tools/isac/MathEngine/step.sml	Sat Feb 04 16:49:08 2023 +0100
     1.2 +++ b/test/Tools/isac/MathEngine/step.sml	Sat Feb 04 17:00:25 2023 +0100
     1.3 @@ -226,7 +226,7 @@
     1.4      val pos' as (p', _) = (lev_on p, Res);
     1.5  
     1.6  if pos = ([1], Res) then () else error "Step.inconsistent changed 2a";
     1.7 -if UnparseC.term_in_ctxt @{context} f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
     1.8 +if UnparseC.term @{context} f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
     1.9    then () else error "Step.inconsistent changed 2b";
    1.10  
    1.11      val (pt,c) = 
    1.12 @@ -252,7 +252,7 @@
    1.13  val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
    1.14  if p = ([2], Res) andalso 
    1.15    get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", "")) andalso
    1.16 -  UnparseC.term_in_ctxt @{context} f =
    1.17 +  UnparseC.term @{context} f =
    1.18    "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos ?u * d_d x ?_dummy_2"
    1.19    (*WAS with old findFillpatterns:
    1.20    "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos ?_dummy_2 * d_d x ?_dummy_3"