1.1 --- a/src/Tools/isac/ME/inform.sml	Thu Aug 19 15:41:56 2010 +0200
     1.2 +++ b/src/Tools/isac/ME/inform.sml	Fri Aug 20 12:25:37 2010 +0200
     1.3 @@ -227,7 +227,7 @@
     1.4  (* val itm as (i,v,b,f, Cor ((d,ts),_)) = hd probl;
     1.5     *)
     1.6      (let val t = (term_of o comp_dts (Isac "delay")) (d,ts);
     1.7 -	 val s = Sign.string_of_term (sign_of dI) t;
     1.8 +	 val s = Syntax.string_of_term (thy2ctxt dI) t;
     1.9       (*this    ^ should raise the exn on unability of re-parsing dts*)
    1.10       in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
    1.11    | parsitm dI (itm as (i,v,b,f, Syn str)) =
    1.12 @@ -238,17 +238,17 @@
    1.13       in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str))
    1.14    | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) =
    1.15      (let val t = (term_of o comp_dts (Isac "delay")) (d,ts);
    1.16 -	 val s = Sign.string_of_term (sign_of dI) t;
    1.17 +	 val s = Syntax.string_of_term (thy2ctxt dI) t;
    1.18       (*this    ^ should raise the exn on unability of re-parsing dts*)
    1.19       in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
    1.20    | parsitm dI (itm as (i,v,_,f, Sup (d,ts))) =
    1.21      (let val t = (term_of o comp_dts (Isac"delay" )) (d,ts);
    1.22 -	 val s = Sign.string_of_term (sign_of dI) t;
    1.23 +	 val s = Syntax.string_of_term (thy2ctxt dI) t;
    1.24       (*this    ^ should raise the exn on unability of re-parsing dts*)
    1.25       in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
    1.26    | parsitm dI (itm as (i,v,_,f, Mis (d,t'))) =
    1.27      (let val t = d $ t';
    1.28 -	 val s = Sign.string_of_term (sign_of dI) t;
    1.29 +	 val s = Syntax.string_of_term (thy2ctxt dI) t;
    1.30       (*this    ^ should raise the exn on unability of re-parsing dts*)
    1.31       in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
    1.32    | parsitm dI (itm as (i,v,_,f, Par _)) =