1.1 --- a/src/Tools/isac/ME/calchead.sml	Tue Aug 17 09:05:51 2010 +0200
     1.2 +++ b/src/Tools/isac/ME/calchead.sml	Wed Aug 18 13:40:09 2010 +0200
     1.3 @@ -1177,7 +1177,7 @@
     1.4  	  | eq_untouched _ _ = false;
     1.5  	    val ppc' = 
     1.6  		(
     1.7 -		 (*writeln("### insert_ppc: itm= "^(itm2str itm));*)       
     1.8 +		 (*writeln("### insert_ppc: itm= "^(itm2str_ itm));*)       
     1.9  		 case seek_ppc (#1 itm) ppc of
    1.10  		     (* val Some xxx = seek_ppc (#1 itm) ppc;
    1.11  		        *)
    1.12 @@ -1276,7 +1276,7 @@
    1.13        (* val Add itm = appl_add thy sel oris pbl ppc ct;
    1.14           *)
    1.15  	let
    1.16 -	    (*val _= writeln("###specify_additem: itm= "^(itm2str itm));*)
    1.17 +	    (*val _= writeln("###specify_additem: itm= "^(itm2str_ itm));*)
    1.18  	  val pbl' = insert_ppc thy itm pbl
    1.19  	  val ((p,Pbl),_,_,pt') = 
    1.20  	      generate1 thy (case sel of
    1.21 @@ -1507,7 +1507,7 @@
    1.22  (* val Add itm = appl_add thy sel oris pbl ppc ct;
    1.23     *)
    1.24  	   let
    1.25 -	       (*val _=writeln("###nxt_specif_additem: itm= "^(itm2str itm));*)
    1.26 +	       (*val _=writeln("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
    1.27  	       val pbl' = insert_ppc thy itm pbl
    1.28  	       val (tac,tac_) = 
    1.29  		   case sel of
    1.30 @@ -1939,8 +1939,8 @@
    1.31  (*
    1.32    writeln (oris2str pors);
    1.33  
    1.34 -  writeln (itms2str thy pits);
    1.35 -  writeln (itms2str thy mits);
    1.36 +  writeln (itms2str_ thy pits);
    1.37 +  writeln (itms2str_ thy mits);
    1.38     *)
    1.39  
    1.40