src/HOLCF/IOA/meta_theory/automaton.ML
changeset 36692 54b64d4ad524
parent 32960 69916a850301
child 36960 01594f816e3a
     1.1 --- a/src/HOLCF/IOA/meta_theory/automaton.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOLCF/IOA/meta_theory/automaton.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -211,11 +211,11 @@
     1.4  
     1.5  (* used by write_alts *)
     1.6  fun write_alt thy (chead,tr) inp out int [] =
     1.7 -if (chead mem inp) then
     1.8 +if member (op =) inp chead then
     1.9  (
    1.10  error("Input action " ^ tr ^ " was not specified")
    1.11  ) else (
    1.12 -if (chead mem (out@int)) then
    1.13 +if member (op =) out chead orelse member (op =) int chead then
    1.14  (writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else ();
    1.15  (tr ^ " => False",tr ^ " => False")) |
    1.16  write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) =
    1.17 @@ -227,9 +227,9 @@
    1.18  occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r);
    1.19  in
    1.20  if (chead=(hd_of a)) then 
    1.21 -(if ((chead mem inp) andalso e) then (
    1.22 +(if member (op =) inp chead andalso e then (
    1.23  error("Input action " ^ b ^ " has a precondition")
    1.24 -) else (if (chead mem (inp@out@int)) then 
    1.25 +) else (if member (op =) (inp@out@int) chead then 
    1.26      (if (occurs_again chead r) then (
    1.27  error("Two specifications for action: " ^ b)
    1.28      ) else (b ^ " => " ^ c,b ^ " => " ^ d))
    1.29 @@ -275,7 +275,7 @@
    1.30  check_free_primed _ = [];
    1.31  
    1.32  fun overlap [] _ = true |
    1.33 -overlap (a::r) l = if (a mem l) then (
    1.34 +overlap (a::r) l = if member (op =) l a then (
    1.35  error("Two occurences of action " ^ a ^ " in automaton signature")
    1.36  ) else (overlap r l);
    1.37