diff -r 5f462dfaf130 -r 5c7a69cef18b Trancl.ML
--- a/Trancl.ML	Fri Jun 24 15:11:39 1994 +0200
+++ b/Trancl.ML	Wed Jun 29 12:04:04 1994 +0200
@@ -151,7 +151,7 @@
     "[| <a::'a,b> : r^*;  (a = b) ==> P; 	\
 \	!!y.[| <a,y> : r^*; <y,b> : r |] ==> P 	\
 \    |] ==> P";
-by (subgoal_tac "a::'a = b  | (? y. <a,y> : r^* & <y,b> : r)" 1);
+by (subgoal_tac "(a::'a) = b  | (? y. <a,y> : r^* & <y,b> : r)" 1);
 by (rtac (major RS rtrancl_induct) 2);
 by (fast_tac (set_cs addIs prems) 2);
 by (fast_tac (set_cs addIs prems) 2);