1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Tue Aug 10 10:27:15 2021 +0200
1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Tue Aug 10 11:01:18 2021 +0200
1.3 @@ -29,7 +29,7 @@
1.4 > val t = (Thm.term_of o the o (TermC.parse thy)) "#2 \<up> #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 (ThyC.to_ctxt thy) t';
1.8 +> Syntax.string_of_term (Proof_Context.init_global thy) t';
1.9 *)
1.10 (******************************************************************)
1.11 (* ------------------------------------- *)