--- a/src/HOL/UNITY/SubstAx.ML Mon May 03 10:57:14 1999 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Mon May 03 11:18:11 1999 +0200
@@ -397,7 +397,7 @@
qed "Completion";
-Goal "[| finite I |] \
+Goal "finite I \
\ ==> (ALL i:I. F : (A i) LeadsTo (A' i Un C)) --> \
\ (ALL i:I. F : (A' i) Co (A' i Un C)) --> \
\ F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)";
@@ -406,7 +406,7 @@
by (Clarify_tac 1);
by (dtac ball_Constrains_INT 1);
by (asm_full_simp_tac (simpset() addsimps [Completion]) 1);
-qed "Finite_completion";
+qed_spec_mp "Finite_completion";
(*proves "ensures/leadsTo" properties when the program is specified*)
--- a/src/HOL/UNITY/WFair.ML Mon May 03 10:57:14 1999 +0200
+++ b/src/HOL/UNITY/WFair.ML Mon May 03 11:18:11 1999 +0200
@@ -528,5 +528,5 @@
by (Clarify_tac 1);
by (dtac ball_constrains_INT 1);
by (asm_full_simp_tac (simpset() addsimps [completion]) 1);
-qed "finite_completion";
+qed_spec_mp "finite_completion";