src/CTT/CTT.ML

     (rtac sym_type 2),
     (ALLGOALS (resolve_tac prems)) ]);
 
 (*Simplify the parameter of a unary type operator.*)
 qed_goal "subst_eqtyparg" CTT.thy
-    "a=c : A ==> (!!z.z:A ==> B(z) type) ==> B(a)=B(c)"
+    "a=c : A ==> (!!z. z:A ==> B(z) type) ==> B(a)=B(c)"
  (fn prems=>
   [ (rtac subst_typeL 1),
     (rtac refl_type 2),
     (ALLGOALS (resolve_tac prems)),
     (assume_tac 1) ]);