# HG changeset patch
# User wenzelm
# Date 1026986729 -7200
# Node ID eff0ede61da157795b1fd917c4e78f74e0355f60
# Parent  b7464ca2ebbb715b32a507f18f25e90bf440ad1c
quantify LC (conflict with const name of HOL);

diff -r b7464ca2ebbb -r eff0ede61da1 src/HOLCF/IOA/meta_theory/Abstraction.ML
--- 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) ; \
diff -r b7464ca2ebbb -r eff0ede61da1 src/HOLCF/IOA/meta_theory/LiveIOA.ML
--- 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";