diff -r 886655a150f6 -r d1b97708d5eb src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/CTT/CTT.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -397,13 +397,13 @@
 
 (*Simplify the parameter of a unary type operator.*)
 lemma subst_eqtyparg:
-  assumes "a=c : A"
-    and "!!z. z:A ==> B(z) type"
+  assumes 1: "a=c : A"
+    and 2: "!!z. z:A ==> B(z) type"
   shows "B(a)=B(c)"
 apply (rule subst_typeL)
 apply (rule_tac [2] refl_type)
-apply (rule prems)
-apply assumption
+apply (rule 1)
+apply (erule 2)
 done
 
 (*Simplification rules for Constructive Type Theory*)