--- a/src/HOL/HOLCF/IOA/ABP/Check.ML Tue Aug 23 16:41:16 2011 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Check.ML Tue Aug 23 16:53:05 2011 +0200
@@ -112,21 +112,21 @@
------------------------------------*)
fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
- let fun prec x = (Output.raw_stdout ","; pre x)
+ let fun prec x = (Output.physical_stdout ","; pre x)
in
(case lll of
- [] => (Output.raw_stdout lpar; Output.raw_stdout rpar)
- | x::lll => (Output.raw_stdout lpar; pre x; List.app prec lll; Output.raw_stdout rpar))
+ [] => (Output.physical_stdout lpar; Output.physical_stdout rpar)
+ | x::lll => (Output.physical_stdout lpar; pre x; List.app prec lll; Output.physical_stdout rpar))
end;
-fun pr_bool true = Output.raw_stdout "true"
-| pr_bool false = Output.raw_stdout "false";
+fun pr_bool true = Output.physical_stdout "true"
+| pr_bool false = Output.physical_stdout "false";
-fun pr_msg m = Output.raw_stdout "m"
-| pr_msg n = Output.raw_stdout "n"
-| pr_msg l = Output.raw_stdout "l";
+fun pr_msg m = Output.physical_stdout "m"
+| pr_msg n = Output.physical_stdout "n"
+| pr_msg l = Output.physical_stdout "l";
-fun pr_act a = Output.raw_stdout (case a of
+fun pr_act a = Output.physical_stdout (case a of
Next => "Next"|
S_msg(ma) => "S_msg(ma)" |
R_msg(ma) => "R_msg(ma)" |
@@ -135,17 +135,17 @@
S_ack(b) => "S_ack(b)" |
R_ack(b) => "R_ack(b)");
-fun pr_pkt (b,ma) = (Output.raw_stdout "<"; pr_bool b;Output.raw_stdout ", "; pr_msg ma; Output.raw_stdout ">");
+fun pr_pkt (b,ma) = (Output.physical_stdout "<"; pr_bool b;Output.physical_stdout ", "; pr_msg ma; Output.physical_stdout ">");
val pr_bool_list = print_list("[","]",pr_bool);
val pr_msg_list = print_list("[","]",pr_msg);
val pr_pkt_list = print_list("[","]",pr_pkt);
fun pr_tuple (env,p,a,q,b,ch1,ch2) =
- (Output.raw_stdout "{"; pr_bool env; Output.raw_stdout ", "; pr_msg_list p; Output.raw_stdout ", ";
- pr_bool a; Output.raw_stdout ", "; pr_msg_list q; Output.raw_stdout ", ";
- pr_bool b; Output.raw_stdout ", "; pr_pkt_list ch1; Output.raw_stdout ", ";
- pr_bool_list ch2; Output.raw_stdout "}");
+ (Output.physical_stdout "{"; pr_bool env; Output.physical_stdout ", "; pr_msg_list p; Output.physical_stdout ", ";
+ pr_bool a; Output.physical_stdout ", "; pr_msg_list q; Output.physical_stdout ", ";
+ pr_bool b; Output.physical_stdout ", "; pr_pkt_list ch1; Output.physical_stdout ", ";
+ pr_bool_list ch2; Output.physical_stdout "}");