1.1 --- a/src/Tools/isac/ME/inform.sml	Tue Aug 17 09:05:51 2010 +0200
     1.2 +++ b/src/Tools/isac/ME/inform.sml	Wed Aug 18 13:40:09 2010 +0200
     1.3 @@ -252,7 +252,7 @@
     1.4       (*this    ^ should raise the exn on unability of re-parsing dts*)
     1.5       in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
     1.6    | parsitm dI (itm as (i,v,_,f, Par _)) = 
     1.7 -    raise error ("parsitm ("^itm2str dI itm^
     1.8 +    raise error ("parsitm ("^itm2str_ dI itm^
     1.9  		 "): Par should be internal");
    1.10  
    1.11  (*separate a list to a pair of elements that do NOT satisfy the predicate,
    1.12 @@ -358,7 +358,7 @@
    1.13         (#1 (some_spec ospec spec), oris, []:itm list,
    1.14  	((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
    1.15     val iii = appl_adds dI oris ppc pbt (selct::ss); 
    1.16 -   writeln(itms2str thy iii);
    1.17 +   writeln(itms2str_ thy iii);
    1.18  
    1.19   val itm = appl_add' dI oris ppc pbt selct;
    1.20   val ppc = insert_ppc' itm ppc;
    1.21 @@ -370,7 +370,7 @@
    1.22   val _::selct::ss = (selct::ss);
    1.23   val itm = appl_add' dI oris ppc pbt selct;
    1.24   val ppc = insert_ppc' itm ppc;
    1.25 - writeln(itms2str thy ppc);
    1.26 + writeln(itms2str_ thy ppc);
    1.27  
    1.28   val _::selct::ss = (selct::ss);
    1.29   val itm = appl_add' dI oris ppc pbt selct;
    1.30 @@ -393,7 +393,7 @@
    1.31  
    1.32  fun par2fstr ((_,_,_,f, Par s):itm) = (f, s)
    1.33    | par2fstr itm = raise error ("par2fstr: called with "^
    1.34 -			      itm2str (assoc_thy "Isac.thy") itm);
    1.35 +			      itm2str_ (assoc_thy "Isac.thy") itm);
    1.36  fun itms2fstr ((_,_,_,f, Cor ((d,ts),_)):itm) = (f, comp_dts'' (d,ts))
    1.37    | itms2fstr (_,_,_,f, Syn str) = (f, str)
    1.38    | itms2fstr (_,_,_,f, Typ str) = (f, str)
    1.39 @@ -401,7 +401,7 @@
    1.40    | itms2fstr (_,_,_,f, Sup (d,ts)) = (f, comp_dts'' (d,ts))
    1.41    | itms2fstr (_,_,_,f, Mis (d,t)) = (f, term2str (d $ t))
    1.42    | itms2fstr (itm as (_,_,_,f, Par _)) = 
    1.43 -    raise error ("parsitm ("^itm2str (assoc_thy "Isac.thy") itm^
    1.44 +    raise error ("parsitm ("^itm2str_ (assoc_thy "Isac.thy") itm^
    1.45  		 "): Par should be internal");
    1.46  
    1.47  fun imodel2fstr iitems =