1.1 --- a/src/HOL/UNITY/SubstAx.ML	Mon May 03 10:57:14 1999 +0200
     1.2 +++ b/src/HOL/UNITY/SubstAx.ML	Mon May 03 11:18:11 1999 +0200
     1.3 @@ -397,7 +397,7 @@
     1.4  qed "Completion";
     1.5  
     1.6  
     1.7 -Goal "[| finite I |] \
     1.8 +Goal "finite I \
     1.9  \     ==> (ALL i:I. F : (A i) LeadsTo (A' i Un C)) -->  \
    1.10  \         (ALL i:I. F : (A' i) Co (A' i Un C)) --> \
    1.11  \         F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)";
    1.12 @@ -406,7 +406,7 @@
    1.13  by (Clarify_tac 1);
    1.14  by (dtac ball_Constrains_INT 1);
    1.15  by (asm_full_simp_tac (simpset() addsimps [Completion]) 1); 
    1.16 -qed "Finite_completion";
    1.17 +qed_spec_mp "Finite_completion";
    1.18  
    1.19  
    1.20  (*proves "ensures/leadsTo" properties when the program is specified*)

     2.1 --- a/src/HOL/UNITY/WFair.ML	Mon May 03 10:57:14 1999 +0200
     2.2 +++ b/src/HOL/UNITY/WFair.ML	Mon May 03 11:18:11 1999 +0200
     2.3 @@ -528,5 +528,5 @@
     2.4  by (Clarify_tac 1);
     2.5  by (dtac ball_constrains_INT 1);
     2.6  by (asm_full_simp_tac (simpset() addsimps [completion]) 1); 
     2.7 -qed "finite_completion";
     2.8 +qed_spec_mp "finite_completion";
     2.9