1.1 --- a/src/Tools/isac/ME/ptyps.sml	Thu Aug 19 12:00:46 2010 +0200
     1.2 +++ b/src/Tools/isac/ME/ptyps.sml	Thu Aug 19 12:08:42 2010 +0200
     1.3 @@ -15,16 +15,16 @@
     1.4  (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*)
     1.5  
     1.6  fun itm_2item thy (Cor ((d,ts),_)) = 
     1.7 -    Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts)))
     1.8 +    Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
     1.9    | itm_2item _ (Syn c)            = SyntaxE c
    1.10    | itm_2item _ (Typ c)            = TypeE c
    1.11    | itm_2item thy (Inc ((d,ts),_)) = 
    1.12 -    Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts)))
    1.13 +    Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
    1.14    | itm_2item thy (Sup (d,ts))     = 
    1.15 -    Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy (d,ts)))
    1.16 +    Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
    1.17    | itm_2item _ (Mis (d,pid))   =
    1.18 -    Missing (Syntax.string_of_term (ctxt_Isac"") d ^" "^ 
    1.19 -	     Syntax.string_of_term (ctxt_Isac"") pid);
    1.20 +    Missing (Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^ 
    1.21 +	     Syntax.string_of_term (thy2ctxt' "Isac") pid);
    1.22  
    1.23  
    1.24  (* --- 8.3.00
    1.25 @@ -99,7 +99,7 @@
    1.26       else (e_term, [t])    (*??? 9.01 just copied*)
    1.27    end)
    1.28    handle _ => raise error ("split_dsc: called with "^
    1.29 -			   (Syntax.string_of_term (ctxt_Isac"") t));
    1.30 +			   (Syntax.string_of_term (thy2ctxt' "Isac") t));
    1.31  (*
    1.32  > val t1 = (term_of o the o (parse thy)) "errorBound err_";
    1.33  > split_dsc t1;
    1.34 @@ -134,14 +134,14 @@
    1.35  
    1.36  
    1.37  (*create output-string for itm_*)
    1.38 -fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
    1.39 +fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
    1.40    | itm_out thy (Syn c)      = c
    1.41    | itm_out thy (Typ c)      = c
    1.42 -  | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
    1.43 -  | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
    1.44 +  | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
    1.45 +  | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
    1.46    | itm_out thy (Mis (d,pid)) = 
    1.47 -    Syntax.string_of_term (ctxt_Isac"") d ^" "^ 
    1.48 -    Syntax.string_of_term (ctxt_Isac"") pid;
    1.49 +    Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^ 
    1.50 +    Syntax.string_of_term (thy2ctxt' "Isac") pid;
    1.51  
    1.52  (*22.11.00 unused				     
    1.53  fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*)
    1.54 @@ -163,15 +163,15 @@
    1.55  *)
    1.56  (*--3.3.00
    1.57  fun itm2item ((_,_,_,_,Cor (d,ts)):itm) = 
    1.58 -	      Correct (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
    1.59 +	      Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
    1.60    | itm2item (_,_,_,_,Syn (c))    = SyntaxE c
    1.61    | itm2item (_,_,_,_,Typ (c))    = TypeE c
    1.62    | itm2item (_,_,_,_,Fal (d,ts)) = 
    1.63 -	      False (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
    1.64 +	      False (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
    1.65    | itm2item (_,_,_,_,Inc (d,ts)) = 
    1.66 -	      Incompl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)))
    1.67 +	      Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
    1.68    | itm2item (_,_,_,_,Sup (d,ts)) = 
    1.69 -	      Superfl (Syntax.string_of_term (ctxt_Isac"") (comp_dts thy(d,ts)));
    1.70 +	      Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)));
    1.71  *)
    1.72  
    1.73  fun boolterm2item (true, term) = Correct (term2str term)
    1.74 @@ -199,7 +199,7 @@
    1.75  	      then ("#Relate",d,ts)
    1.76  	    else ("#undef",d,ts);
    1.77  (* 28.1.00      raise error ("add_field: '"^
    1.78 -			      (Syntax.string_of_term (ctxt_Isac"") d)^
    1.79 +			      (Syntax.string_of_term (thy2ctxt' "Isac") d)^
    1.80  			      "' not in ppc-description ");         *)
    1.81   ------9.3. *)
    1.82  
    1.83 @@ -211,7 +211,7 @@
    1.84         [(fi,(dsc,_))] => (fi,d,ts)
    1.85       | [] => ("#undef",d,ts)   (*may come with met.ppc*)
    1.86       | _ => raise error ("add_field: "^
    1.87 -			 (Syntax.string_of_term (ctxt_Isac"") d)^
    1.88 +			 (Syntax.string_of_term (thy2ctxt' "Isac") d)^
    1.89  			 " more than once in pbt")
    1.90    end;
    1.91  
    1.92 @@ -226,10 +226,10 @@
    1.93  	[(fi,(dsc,_))] => [(i,v,fi,d,ts)]
    1.94        | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)    
    1.95        (*raise error ("add_field': "^
    1.96 -		     (Syntax.string_of_term (ctxt_Isac"") d)^
    1.97 +		     (Syntax.string_of_term (thy2ctxt' "Isac") d)^
    1.98  		     " not in met"*)
    1.99        | _ => raise error ("add_field': "^
   1.100 -			 (Syntax.string_of_term (ctxt_Isac"") d)^
   1.101 +			 (Syntax.string_of_term (thy2ctxt' "Isac") d)^
   1.102  			 " more than once in met");
   1.103    in (flat ((map (repl mpc)) ori)):ori list end;
   1.104