--- a/ProgTutorial/Package/Ind_Extensions.thy	Tue Nov 24 22:55:44 2009 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Wed Nov 25 21:00:31 2009 +0100
@@ -86,10 +86,10 @@
   \begin{center}\small
   \mprset{flushleft}
   \mbox{\inferrule{
-             @{thm_style prem1  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
-             @{thm_style prem2  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
-             @{thm_style prem3  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}
-            {@{thm_style concl  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}}  
+             @{thm (prem1)  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
+             @{thm (prem2)  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
+             @{thm (prem3)  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}
+            {@{thm (concl)  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}}  
   \end{center}
 
   But this does not correspond to the induction principle we derived by hand, which