diff -r dfec2cf32f77 -r 862f35fdb091 src/Tools/isac/ME/ptyps.sml
--- a/src/Tools/isac/ME/ptyps.sml	Thu Aug 19 12:00:46 2010 +0200
+++ b/src/Tools/isac/ME/ptyps.sml	Thu Aug 19 12:08:42 2010 +0200
@@ -15,16 +15,16 @@
 (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*)
 
 fun itm_2item thy (Cor ((d,ts),_)) = 
-    Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts)))
+    Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
   | itm_2item _ (Syn c)            = SyntaxE c
   | itm_2item _ (Typ c)            = TypeE c
   | itm_2item thy (Inc ((d,ts),_)) = 
-    Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts)))
+    Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
   | itm_2item thy (Sup (d,ts))     = 
-    Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts)))
+    Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
   | itm_2item _ (Mis (d,pid))   =
-    Missing (Syntax.string_of_term (ctxt_Isac"") d ^" "^ 
-	     Syntax.string_of_term (ctxt_Isac"") pid);
+    Missing (Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^ 
+	     Syntax.string_of_term (thy2ctxt' "Isac") pid);
 
 
 (* --- 8.3.00
@@ -99,7 +99,7 @@
      else (e_term, [t])    (*??? 9.01 just copied*)
   end)
   handle _ => raise error ("split_dsc: called with "^
-			   (Syntax.string_of_term (ctxt_Isac"") t));
+			   (Syntax.string_of_term (thy2ctxt' "Isac") t));
 (*
 > val t1 = (term_of o the o (parse thy)) "errorBound err_";
 > split_dsc t1;
@@ -134,14 +134,14 @@
 
 
 (*create output-string for itm_*)
-fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
+fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
   | itm_out thy (Syn c)      = c
   | itm_out thy (Typ c)      = c
-  | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
-  | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
+  | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
+  | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
   | itm_out thy (Mis (d,pid)) = 
-    Syntax.string_of_term (ctxt_Isac"") d ^" "^ 
-    Syntax.string_of_term (ctxt_Isac"") pid;
+    Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^ 
+    Syntax.string_of_term (thy2ctxt' "Isac") pid;
 
 (*22.11.00 unused				     
 fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*)
@@ -163,15 +163,15 @@
 *)
 (*--3.3.00
 fun itm2item ((_,_,_,_,Cor (d,ts)):itm) = 
-	      Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
+	      Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
   | itm2item (_,_,_,_,Syn (c))    = SyntaxE c
   | itm2item (_,_,_,_,Typ (c))    = TypeE c
   | itm2item (_,_,_,_,Fal (d,ts)) = 
-	      False (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
+	      False (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
   | itm2item (_,_,_,_,Inc (d,ts)) = 
-	      Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
+	      Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
   | itm2item (_,_,_,_,Sup (d,ts)) = 
-	      Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)));
+	      Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)));
 *)
 
 fun boolterm2item (true, term) = Correct (term2str term)
@@ -199,7 +199,7 @@
 	      then ("#Relate",d,ts)
 	    else ("#undef",d,ts);
 (* 28.1.00      raise error ("add_field: '"^
-			      (Syntax.string_of_term (ctxt_Isac"") d)^
+			      (Syntax.string_of_term (thy2ctxt' "Isac") d)^
 			      "' not in ppc-description ");         *)
  ------9.3. *)
 
@@ -211,7 +211,7 @@
        [(fi,(dsc,_))] => (fi,d,ts)
      | [] => ("#undef",d,ts)   (*may come with met.ppc*)
      | _ => raise error ("add_field: "^
-			 (Syntax.string_of_term (ctxt_Isac"") d)^
+			 (Syntax.string_of_term (thy2ctxt' "Isac") d)^
 			 " more than once in pbt")
   end;
 
@@ -226,10 +226,10 @@
 	[(fi,(dsc,_))] => [(i,v,fi,d,ts)]
       | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)    
       (*raise error ("add_field': "^
-		     (Syntax.string_of_term (ctxt_Isac"") d)^
+		     (Syntax.string_of_term (thy2ctxt' "Isac") d)^
 		     " not in met"*)
       | _ => raise error ("add_field': "^
-			 (Syntax.string_of_term (ctxt_Isac"") d)^
+			 (Syntax.string_of_term (thy2ctxt' "Isac") d)^
 			 " more than once in met");
   in (flat ((map (repl mpc)) ori)):ori list end;