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";