1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Tue Jan 31 12:47:11 2023 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Tue Jan 31 16:29:53 2023 +0100
     1.3 @@ -307,7 +307,7 @@
     1.4      in ord end
     1.5  and terms_ord x i pr (ts, us) = 
     1.6      let
     1.7 -      val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
     1.8 +      val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms_in_ctxt @{context} ts ^ ", " ^ UnparseC.terms_in_ctxt @{context} us ^ ")") else ();
     1.9        val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
    1.10        val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
    1.11      in ord end
    1.12 @@ -487,8 +487,8 @@
    1.13  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.14  val asm = Ctree.get_assumptions pt p;
    1.15  if f2str f = "[]" andalso 
    1.16 -  UnparseC.terms asm = "[\"lhs (2 + - 1 * x + x \<up> 2 = 0) is_poly_in x\", " ^
    1.17 -    "\"lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2\"]" then ()
    1.18 +  UnparseC.terms_in_ctxt @{context} asm = "[lhs (2 + - 1 * x + x \<up> 2 = 0) is_poly_in x, " ^
    1.19 +    "lhs (2 + - 1 * x + x \<up> 2 = 0) has_degree_in x = 2]" then ()
    1.20  else error "polyeq.sml: diff.behav. in 2 +(- 1)*x + x \<up> 2 = 0";
    1.21  
    1.22  "----------- equality (- 2 +(- 1)*x + 1*x \<up> 2 = 0) ---------------------------------------------";