diff -r 825877190618 -r 74919e8f221c src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Univ.ML	Wed Jul 15 14:19:02 1998 +0200
@@ -73,7 +73,7 @@
 qed "Node_K0_I";
 
 Goalw [Node_def,Push_def]
-    "!!p. p: Node ==> apfst (Push i) p : Node";
+    "p: Node ==> apfst (Push i) p : Node";
 by (blast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
 qed "Node_Push_I";
 
@@ -489,7 +489,7 @@
 (*** Equality for Cartesian Product ***)
 
 Goalw [dprod_def]
-    "!!r s. [| (M,M'):r;  (N,N'):s |] ==> (M$N, M'$N') : r<**>s";
+    "[| (M,M'):r;  (N,N'):s |] ==> (M$N, M'$N') : r<**>s";
 by (Blast_tac 1);
 qed "dprodI";