--- a/ProgTutorial/Package/Ind_Code.thy	Tue Aug 25 00:07:37 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Mon Sep 28 01:21:27 2009 +0200
@@ -239,12 +239,14 @@
 *}
 
 ML{*fun inst_spec ctrm = 
-  Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}
+  Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] 
+    @{thm spec}*}
 
 text {*
-  This helper function instantiates the @{text "?x"} in the theorem 
-  @{thm spec} with a given @{ML_type cterm}. We call this helper function
-  in the following tactic.\label{fun:instspectac}.
+  This helper function uses the function @{ML_ind instantiate' in Drule}
+  and instantiates the @{text "?x"} in the theorem @{thm spec} with a given
+  @{ML_type cterm}. We call this helper function in the following
+  tactic.\label{fun:instspectac}.
 *}
 
 ML{*fun inst_spec_tac ctrms =