quantify LC (conflict with const name of HOL);

--- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Thu Jul 18 10:37:55 2002 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Thu Jul 18 12:05:29 2002 +0200
@@ -249,7 +249,7 @@
 qed"AbsRuleA1";
 
 
-Goal "[| inp(C)=inp(A); out(C)=out(A); \
+Goal "!!LC. [| inp(C)=inp(A); out(C)=out(A); \
 \                  inp(Q)=inp(P); out(Q)=out(P); \
 \                  is_live_abstraction h1 (C,LC) (A,LA); \
 \                  live_implements (A,LA) (Q,LQ) ; \

--- a/src/HOLCF/IOA/meta_theory/LiveIOA.ML	Thu Jul 18 10:37:55 2002 +0200
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.ML	Thu Jul 18 12:05:29 2002 +0200
@@ -9,7 +9,7 @@
 Delsimps [split_paired_Ex];
 
 Goalw [live_implements_def] 
-"[| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] \
+"!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] \
 \     ==> live_implements (A,LA) (C,LC)"; 
 by Auto_tac;
 qed"live_implements_trans";