1.1 --- a/test/Tools/isac/IsacKnowledge/integrate.sml	Thu Aug 19 15:41:56 2010 +0200
     1.2 +++ b/test/Tools/isac/IsacKnowledge/integrate.sml	Fri Aug 20 12:25:37 2010 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4  "----------- parsing ---------------------------------------------";
     1.5  "----------- parsing ---------------------------------------------";
     1.6  fun str2term str = (term_of o the o (parse Integrate.thy)) str;
     1.7 -fun term2s t = Sign.string_of_term (sign_of Integrate.thy) t;
     1.8 +fun term2s t = Syntax.string_of_term (thy2ctxt' "Integrate") t;
     1.9      
    1.10  val t = str2term "Integral x D x";
    1.11  val t = str2term "Integral x^^^2 D x";
    1.12 @@ -576,4 +576,4 @@
    1.13  (* WN070703 does not work like Diff due to error in next-pos
    1.14  if p = ([], Res) andalso term2str res = "5 * a" then ()
    1.15  else raise error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";
    1.16 -*)
    1.17 \ No newline at end of file
    1.18 +*)