test/Tools/isac/OLDTESTS/root-equ.sml
changeset 60360 49680d595342
parent 60340 0ee698b0a703
child 60387 8e46f61fdb15
     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  (*                  -------------------------------------         *)