1.1 --- a/src/Tools/isac/Interpret/inform.sml Fri Oct 08 18:58:24 2010 +0200
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Sat Oct 09 16:03:49 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 = (comp_dts (Isac "delay")) (d,ts);
1.7 - val s = Syntax.string_of_term (thy2ctxt dI) t;
1.8 + val s = Print_Mode.setmp [] (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 = (comp_dts (Isac "delay")) (d,ts);
1.16 - val s = Syntax.string_of_term (thy2ctxt dI) t;
1.17 + val s = Print_Mode.setmp [] (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 = (comp_dts (Isac"delay" )) (d,ts);
1.22 - val s = Syntax.string_of_term (thy2ctxt dI) t;
1.23 + val s = Print_Mode.setmp [] (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 = Syntax.string_of_term (thy2ctxt dI) t;
1.29 + val s = Print_Mode.setmp [] (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 _)) =