fixed ML errors;
authorwenzelm
Sat Sep 03 16:46:20 2005 +0200 (2005-09-03 ago)
changeset 1723923ccd02bbba6
parent 17238 b1cf9189104e
child 17240 f197d8e8d4d2
fixed ML errors;
src/HOLCF/IOA/ABP/Check.ML
     1.1 --- a/src/HOLCF/IOA/ABP/Check.ML	Sat Sep 03 16:45:43 2005 +0200
     1.2 +++ b/src/HOLCF/IOA/ABP/Check.ML	Sat Sep 03 16:46:20 2005 +0200
     1.3 @@ -5,6 +5,8 @@
     1.4  The Model Checker.
     1.5  *)
     1.6  
     1.7 +structure Check =
     1.8 +struct
     1.9   
    1.10  (* ----------------------------------------------------------------
    1.11         P r o t o t y p e   M o d e l   C h e c k e r 
    1.12 @@ -27,8 +29,8 @@
    1.13                                   string_of_a a; writeln"";
    1.14                                   string_of_s t;writeln"";writeln"" ));
    1.15                       if t mem checked then unchecked else t ins unchecked)
    1.16 -              in foldl check_sas (unchecked,nexts s a) end;
    1.17 -              val unchecked' = foldl check_sa (unchecked,extacts @ intacts)
    1.18 +              in Library.foldl check_sas (unchecked,nexts s a) end;
    1.19 +              val unchecked' = Library.foldl check_sa (unchecked,extacts @ intacts)
    1.20          in    (if s mem startsI then 
    1.21                      (if hom(s) mem startsS then ()
    1.22                       else writeln("Error: At start states!"))
    1.23 @@ -115,17 +117,17 @@
    1.24    in
    1.25      (case lll of
    1.26        [] => (std_output lpar; std_output rpar)
    1.27 -    | x::lll => (std_output lpar; pre x; seq prec lll; std_output rpar))
    1.28 +    | x::lll => (std_output lpar; pre x; List.app prec lll; std_output rpar))
    1.29     end;
    1.30  
    1.31 -fun pr_bool true = output(std_out,"true")
    1.32 -|   pr_bool false = output(std_out,"false");
    1.33 +fun pr_bool true = std_output "true"
    1.34 +|   pr_bool false = std_output "false";
    1.35  
    1.36 -fun pr_msg m = output(std_out,"m")
    1.37 -|   pr_msg n = output(std_out,"n")
    1.38 -|   pr_msg l = output(std_out,"l");
    1.39 +fun pr_msg m = std_output "m"
    1.40 +|   pr_msg n = std_output "n"
    1.41 +|   pr_msg l = std_output "l";
    1.42  
    1.43 -fun pr_act a = output(std_out, case a of
    1.44 +fun pr_act a = std_output (case a of
    1.45        Next => "Next"|                         
    1.46        S_msg(ma) => "S_msg(ma)"  |
    1.47        R_msg(ma) => "R_msg(ma)"  |
    1.48 @@ -173,3 +175,5 @@
    1.49  fun nexts s A = [(s+1) mod 5];
    1.50  
    1.51  *)
    1.52 +
    1.53 +end;