diff -r 4afbcd008799 -r 6c53fe2519e5 src/Tools/isac/ME/inform.sml
--- a/src/Tools/isac/ME/inform.sml	Tue Aug 17 09:05:51 2010 +0200
+++ b/src/Tools/isac/ME/inform.sml	Wed Aug 18 13:40:09 2010 +0200
@@ -252,7 +252,7 @@
      (*this    ^ should raise the exn on unability of re-parsing dts*)
      in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
   | parsitm dI (itm as (i,v,_,f, Par _)) = 
-    raise error ("parsitm ("^itm2str dI itm^
+    raise error ("parsitm ("^itm2str_ dI itm^
 		 "): Par should be internal");
 
 (*separate a list to a pair of elements that do NOT satisfy the predicate,
@@ -358,7 +358,7 @@
        (#1 (some_spec ospec spec), oris, []:itm list,
 	((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
    val iii = appl_adds dI oris ppc pbt (selct::ss); 
-   writeln(itms2str thy iii);
+   writeln(itms2str_ thy iii);
 
  val itm = appl_add' dI oris ppc pbt selct;
  val ppc = insert_ppc' itm ppc;
@@ -370,7 +370,7 @@
  val _::selct::ss = (selct::ss);
  val itm = appl_add' dI oris ppc pbt selct;
  val ppc = insert_ppc' itm ppc;
- writeln(itms2str thy ppc);
+ writeln(itms2str_ thy ppc);
 
  val _::selct::ss = (selct::ss);
  val itm = appl_add' dI oris ppc pbt selct;
@@ -393,7 +393,7 @@
 
 fun par2fstr ((_,_,_,f, Par s):itm) = (f, s)
   | par2fstr itm = raise error ("par2fstr: called with "^
-			      itm2str (assoc_thy "Isac.thy") itm);
+			      itm2str_ (assoc_thy "Isac.thy") itm);
 fun itms2fstr ((_,_,_,f, Cor ((d,ts),_)):itm) = (f, comp_dts'' (d,ts))
   | itms2fstr (_,_,_,f, Syn str) = (f, str)
   | itms2fstr (_,_,_,f, Typ str) = (f, str)
@@ -401,7 +401,7 @@
   | itms2fstr (_,_,_,f, Sup (d,ts)) = (f, comp_dts'' (d,ts))
   | itms2fstr (_,_,_,f, Mis (d,t)) = (f, term2str (d $ t))
   | itms2fstr (itm as (_,_,_,f, Par _)) = 
-    raise error ("parsitm ("^itm2str (assoc_thy "Isac.thy") itm^
+    raise error ("parsitm ("^itm2str_ (assoc_thy "Isac.thy") itm^
 		 "): Par should be internal");
 
 fun imodel2fstr iitems =