1.1 --- a/test/Tools/isac/Scripts/calculate.sml	Thu Aug 19 15:41:56 2010 +0200
     1.2 +++ b/test/Tools/isac/Scripts/calculate.sml	Fri Aug 20 12:25:37 2010 +0200
     1.3 @@ -36,19 +36,19 @@
     1.4  val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
     1.5  val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
     1.6  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
     1.7 -Sign.string_of_term (sign_of thy) t;
     1.8 +Syntax.string_of_term (thy2ctxt thy) t;
     1.9  (*val it = "(#3 * #4 // #3) ^^^ #2" : string*)
    1.10  val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;
    1.11  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    1.12 -Sign.string_of_term (sign_of thy) t;
    1.13 +Syntax.string_of_term (thy2ctxt thy) t;
    1.14  (*val it = "(#12 // #3) ^^^ #2" : string*)
    1.15  val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
    1.16  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    1.17 -Sign.string_of_term (sign_of thy) t;
    1.18 +Syntax.string_of_term (thy2ctxt thy) t;
    1.19  (*it = "#4 ^^^ #2" : string*)
    1.20  val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
    1.21  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    1.22 -Sign.string_of_term (sign_of thy) t;
    1.23 +Syntax.string_of_term (thy2ctxt thy) t;
    1.24  (*val it = "#16" : string*)
    1.25  if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"
    1.26  else ();
    1.27 @@ -388,22 +388,22 @@
    1.28   val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
    1.29  "1 + 2 = 3";
    1.30   val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    1.31 - Sign.string_of_term (sign_of thy) t;
    1.32 + Syntax.string_of_term (thy2ctxt thy) t;
    1.33  "(3 * 4 / 3) ^^^ 2";
    1.34   val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t;
    1.35  "3 * 4 = 12";
    1.36   val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    1.37 - Sign.string_of_term (sign_of thy) t;
    1.38 + Syntax.string_of_term (thy2ctxt thy) t;
    1.39  "(12 / 3) ^^^ 2";
    1.40   val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t;
    1.41  "12 / 3 = 4";
    1.42   val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    1.43 - Sign.string_of_term (sign_of thy) t;
    1.44 + Syntax.string_of_term (thy2ctxt thy) t;
    1.45  "4 ^^^ 2";
    1.46   val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
    1.47  "4 ^^^ 2 = 16";
    1.48   val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
    1.49 - Sign.string_of_term (sign_of thy) t;
    1.50 + Syntax.string_of_term (thy2ctxt thy) t;
    1.51  "16";
    1.52   if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"
    1.53   else ();