src/HOLCF/IOA/ABP/Check.ML
changeset 36692 54b64d4ad524
parent 35174 e15040ae75d7
child 39733 6d373e9dcb9d
     1.1 --- a/src/HOLCF/IOA/ABP/Check.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOLCF/IOA/ABP/Check.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4    let fun check_s(s,unchecked,checked) =
     1.5          let fun check_sa a unchecked =
     1.6                let fun check_sas t unchecked =
     1.7 -                    (if a mem extacts then
     1.8 +                    (if member (op =) extacts a then
     1.9                            (if transA(hom s,a,hom t) then ( )
    1.10                             else (writeln("Error: Mapping of Externals!");
    1.11                                   string_of_s s; writeln"";
    1.12 @@ -27,11 +27,11 @@
    1.13                                   string_of_s s; writeln"";
    1.14                                   string_of_a a; writeln"";
    1.15                                   string_of_s t;writeln"";writeln"" ));
    1.16 -                     if t mem checked then unchecked else insert (op =) t unchecked)
    1.17 +                     if member (op =) checked t then unchecked else insert (op =) t unchecked)
    1.18                in fold check_sas (nexts s a) unchecked end;
    1.19                val unchecked' = fold check_sa (extacts @ intacts) unchecked
    1.20 -        in    (if s mem startsI then 
    1.21 -                    (if hom(s) mem startsS then ()
    1.22 +        in    (if member (op =) startsI s then 
    1.23 +                    (if member (op =) startsS (hom s) then ()
    1.24                       else writeln("Error: At start states!"))
    1.25                 else ();  
    1.26                 checks(unchecked',s::checked)) end