1.1 --- a/test/Tools/isac/OLDTESTS/script.sml	Thu Aug 19 15:41:56 2010 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/script.sml	Fri Aug 20 12:25:37 2010 +0200
     1.3 @@ -92,19 +92,19 @@
     1.4  val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1);
     1.5  loc_2str l1;
     1.6  (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
     1.7 -Sign.string_of_term (sign_of DiffApp.thy) t1;
     1.8 +Syntax.string_of_term (thy2ctxt' "DiffApp") t1;
     1.9  (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *)
    1.10  
    1.11  val SOME(l2,t2) = same_tacpbl sc l1 (mI2,m2);
    1.12  loc_2str l2;
    1.13  (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
    1.14 -Sign.string_of_term (sign_of DiffApp.thy) t2;
    1.15 +Syntax.string_of_term (thy2ctxt' "DiffApp") t2;
    1.16  (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *)
    1.17  
    1.18  val SOME(l3,t3) = same_tacpbl sc l2 (mI3,m3);
    1.19  loc_2str l3;
    1.20  (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*)
    1.21 -Sign.string_of_term (sign_of DiffApp.thy) t3;
    1.22 +Syntax.string_of_term (thy2ctxt' "DiffApp") t3;
    1.23  (*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*)
    1.24  
    1.25