src/HOLCF/IOA/ABP/Check.ML
changeset 33245 65232054ffd0
parent 22580 d91b4dd651d6
child 35174 e15040ae75d7
     1.1 --- a/src/HOLCF/IOA/ABP/Check.ML	Tue Oct 27 22:55:27 2009 +0100
     1.2 +++ b/src/HOLCF/IOA/ABP/Check.ML	Tue Oct 27 22:56:14 2009 +0100
     1.3 @@ -15,8 +15,8 @@
     1.4  fun check(extacts,intacts,string_of_a,startsI,string_of_s,
     1.5            nexts,hom,transA,startsS) =
     1.6    let fun check_s(s,unchecked,checked) =
     1.7 -        let fun check_sa(unchecked,a) =
     1.8 -              let fun check_sas(unchecked,t) =
     1.9 +        let fun check_sa a unchecked =
    1.10 +              let fun check_sas t unchecked =
    1.11                      (if a mem extacts then
    1.12                            (if transA(hom s,a,hom t) then ( )
    1.13                             else (writeln("Error: Mapping of Externals!");
    1.14 @@ -29,8 +29,8 @@
    1.15                                   string_of_a a; writeln"";
    1.16                                   string_of_s t;writeln"";writeln"" ));
    1.17                       if t mem checked then unchecked else insert (op =) t unchecked)
    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 fold check_sas (nexts s a) unchecked end;
    1.21 +              val unchecked' = fold check_sa (extacts @ intacts) unchecked
    1.22          in    (if s mem startsI then 
    1.23                      (if hom(s) mem startsS then ()
    1.24                       else writeln("Error: At start states!"))