1.1 --- a/test/Tools/isac/Knowledge/rational-2.sml	Tue Jan 10 10:01:05 2023 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml	Tue Jan 10 17:07:53 2023 +0100
     1.3 @@ -718,15 +718,15 @@
     1.4    (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.cut_id)
     1.5  then () else error "first element of revset changed";
     1.6  if
     1.7 -(revsets |> nth 1 |> nth 1 |> Rule.to_string) = "Thm (\"realpow_twoI\", ?r1 \<up> 2 = ?r1 * ?r1)" andalso
     1.8 -(revsets |> nth 1 |> nth 2 |> Rule.to_string) = "Thm (\"#: 9 = 3 \<up> 2\", 9 = 3 \<up> 2)" andalso
     1.9 -(revsets |> nth 1 |> nth 3 |> Rule.to_string) = "Thm (\"#: 6 * x = 2 * (3 * x)\", 6 * x = 2 * (3 * x))"
    1.10 +(revsets |> nth 1 |> nth 1 |> Rule.to_string ctxt) = "Thm (\"realpow_twoI\", ?r1 \<up> 2 = ?r1 * ?r1)" andalso
    1.11 +(revsets |> nth 1 |> nth 2 |> Rule.to_string ctxt) = "Thm (\"#: 9 = 3 \<up> 2\", 9 = 3 \<up> 2)" andalso
    1.12 +(revsets |> nth 1 |> nth 3 |> Rule.to_string ctxt) = "Thm (\"#: 6 * x = 2 * (3 * x)\", 6 * x = 2 * (3 * x))"
    1.13  andalso
    1.14 -(revsets |> nth 1 |> nth 4 |> Rule.to_string) = "Thm (\"#: - 3 * x = - 1 * (3 * x)\", - 3 * x = - 1 * (3 * x))"
    1.15 +(revsets |> nth 1 |> nth 4 |> Rule.to_string ctxt) = "Thm (\"#: - 3 * x = - 1 * (3 * x)\", - 3 * x = - 1 * (3 * x))"
    1.16  andalso
    1.17 -(revsets |> nth 1 |> nth 5 |> Rule.to_string) = "Thm (\"#: 9 = 3 * 3\", 9 = 3 * 3)" andalso
    1.18 -(revsets |> nth 1 |> nth 6 |> Rule.to_string) = "Rls_ (\"sym_order_mult_rls_\")" andalso
    1.19 -(revsets |> nth 1 |> nth 7 |> Rule.to_string) = 
    1.20 +(revsets |> nth 1 |> nth 5 |> Rule.to_string ctxt) = "Thm (\"#: 9 = 3 * 3\", 9 = 3 * 3)" andalso
    1.21 +(revsets |> nth 1 |> nth 6 |> Rule.to_string ctxt) = "Rls_ (\"sym_order_mult_rls_\")" andalso
    1.22 +(revsets |> nth 1 |> nth 7 |> Rule.to_string ctxt) = 
    1.23    "Thm (\"sym_mult.assoc\", ?a * (?b * ?c) = ?a * ?b * ?c)"
    1.24  then () else error "first 7 elements in revset changed"
    1.25  
    1.26 @@ -1581,7 +1581,7 @@
    1.27  
    1.28  (*default_print_depth 99;*) map ((UnparseC.term_in_ctxt ctxt) o #1) der; (*default_print_depth 3;*)
    1.29  "...,(- 1 * b \<up> 2 + a \<up> 2) / (- 2 * (a * b) + a \<up> 2 + (- 1 * b) \<up> 2) ]";
    1.30 -(*default_print_depth 99;*) map (Rule.to_string o #2) der; (*default_print_depth 3;*)
    1.31 +(*default_print_depth 99;*) map ((Rule.to_string ctxt) o #2) der; (*default_print_depth 3;*)
    1.32  (*default_print_depth 99;*) map ((UnparseC.term_in_ctxt ctxt) o #1 o #3) der; (*default_print_depth 3;*)
    1.33  
    1.34  val der = Derive.do_one ctxt Atools_erls rules ro NONE