# HG changeset patch
# User wenzelm
# Date 1131385853 -3600
# Node ID 1e4516e68a582cddb4250dffd61a3c1ac924022d
# Parent  ee6b4d3af498f704beb7f0381f89ac34bce464f4
avoid 'as' as identifier;

diff -r ee6b4d3af498 -r 1e4516e68a58 src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Mon Nov 07 18:32:54 2005 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Mon Nov 07 18:50:53 2005 +0100
@@ -320,13 +320,13 @@
 Delsimps [FilterConc];
 
 
-Goal " [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
-\! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) as &\
-\    Filter (%a. a:ext A)$x = Filter (%a. a:act A)$(as @@ z) \
-\    --> (? x1 x2.  (mksch A B$(as @@ z)$x$y) = (x1 @@ (mksch A B$z$x2$y)) & \
+Goal " [| Finite a_s; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
+\! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) a_s &\
+\    Filter (%a. a:ext A)$x = Filter (%a. a:act A)$(a_s @@ z) \
+\    --> (? x1 x2.  (mksch A B$(a_s @@ z)$x$y) = (x1 @@ (mksch A B$z$x2$y)) & \
 \                   Forall (%x. x:act A & x~:act B) x1 & \
 \                   Finite x1 & x = (x1 @@ x2) & \
-\                   Filter (%a. a:ext A)$x1 = as)";
+\                   Filter (%a. a:ext A)$x1 = a_s)";
 by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1);
 by (etac Seq_Finite_ind  1);
 by (REPEAT (rtac allI 1));