--- a/ProgTutorial/FirstSteps.thy	Thu Mar 19 13:28:16 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Thu Mar 19 17:50:28 2009 +0100
@@ -25,8 +25,6 @@
 
 section {* Including ML-Code *}
 
-
-
 text {*
   The easiest and quickest way to include code in a theory is
   by using the \isacommand{ML}-command. For example:
@@ -154,9 +152,21 @@
 
 text {*
   The easiest way to get the string of a theorem is to transform it
-  into a @{ML_type cterm} using the function @{ML crep_thm}. Theorems
-  also include schematic variables, such as @{text "?P"}, @{text "?Q"}
-  and so on. In order to improve the readability of theorems we convert
+  into a @{ML_type cterm} using the function @{ML crep_thm}. 
+*}
+
+ML{*fun str_of_thm_raw ctxt thm =
+  str_of_cterm ctxt (#prop (crep_thm thm))*}
+
+text {*
+  Theorems also include schematic variables, such as @{text "?P"}, 
+  @{text "?Q"} and so on. 
+
+  @{ML_response_fake [display, gray]
+  "warning (str_of_thm_raw @{context} @{thm conjI})"
+  "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
+
+  In order to improve the readability of theorems we convert
   these schematic variables into free variables using the 
   function @{ML Variable.import_thms}.
 *}
@@ -172,11 +182,20 @@
   str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*}
 
 text {* 
+  Theorem @{thm [source] conjI} looks now as follows
+
+  @{ML_response_fake [display, gray]
+  "warning (str_of_thm_raw @{context} @{thm conjI})"
+  "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
+  
   Again the function @{ML commas} helps with printing more than one theorem. 
 *}
 
 ML{*fun str_of_thms ctxt thms =  
-  commas (map (str_of_thm ctxt) thms)*}
+  commas (map (str_of_thm ctxt) thms)
+
+fun str_of_thms_raw ctxt thms =  
+  commas (map (str_of_thm_raw ctxt) thms)*}
 
 text {*
 (FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling} @{ML Toplevel.debug})
@@ -599,7 +618,8 @@
     Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
                (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 
-  (FIXME: handy functions for constructing terms: @{ML list_comb}, @{ML lambda})
+  (FIXME: handy functions for constructing terms: @{ML list_comb}, @{ML lambda}, 
+  @{ML subst_free})
 *}