1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Wed Apr 15 11:37:43 2020 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Wed Apr 15 13:47:56 2020 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4  > val t = (Thm.term_of o the o (parse thy)) "#2^^^#3";
     1.5  > val eval_fn = the (LibraryC.assoc (!eval_list, "pow"));
     1.6  > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
     1.7 -> Syntax.string_of_term (thy2ctxt thy) t';
     1.8 +> Syntax.string_of_term (ThyC.to_ctxt thy) t';
     1.9  *)
    1.10  (******************************************************************)
    1.11  (*                  -------------------------------------         *)
    1.12 @@ -276,15 +276,15 @@
    1.13  val pt = update_met    pt [] [];
    1.14  (*
    1.15  > get_obj g_spec pt [];
    1.16 -val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec
    1.17 +val it = ("thy_empty_id",["e_pblID"],("thy_empty_id","e_metID")) : spec
    1.18  > val pt = update_domID  pt [] "RatArith";
    1.19  > get_obj g_spec pt [];
    1.20 -val it = ("RatArith",["e_pblID"],("e_domID","e_metID")) : spec
    1.21 +val it = ("RatArith",["e_pblID"],("thy_empty_id","e_metID")) : spec
    1.22  > val pt = update_pblID  pt [] ["RatArith",
    1.23  			      "equations","univariate","square-root"];
    1.24  > get_obj g_spec pt [];
    1.25  ("RatArith",["RatArith","equations","univariate","square-root"],
    1.26 -   ("e_domID","e_metID")) : spec
    1.27 +   ("thy_empty_id","e_metID")) : spec
    1.28  > val pt = update_metID  pt [] ("RatArith","sqrt-equ-test");
    1.29  > get_obj g_spec pt [];
    1.30    ("RatArith",["RatArith","equations","univariate","square-root"],
    1.31 @@ -413,7 +413,7 @@
    1.32  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.33  (* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl");
    1.34  > get_obj g_spec pt (fst p);
    1.35 -val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec*)
    1.36 +val it = ("thy_empty_id",["e_pblID"],("thy_empty_id","e_metID")) : spec*)
    1.37  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.38  (*val nxt = ("Specify_Problem", Specify_Problem *)
    1.39  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;