diff -r 76cdc8f562fc -r d7944bdf7b3f CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Wed Mar 04 13:15:29 2009 +0000
+++ b/CookBook/FirstSteps.thy	Wed Mar 04 13:50:47 2009 +0000
@@ -154,15 +154,26 @@
 
 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}.
+  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
+  these schematic variables into free variables using the 
+  function @{ML Variable.import_thms}.
 *}
 
-ML{*fun str_of_thm ctxt thm =
-  let
-    val {prop, ...} = crep_thm thm
-  in 
-    str_of_cterm ctxt prop
-  end*}
+ML{*fun no_vars ctxt thm =
+let 
+  val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
+in
+  thm'
+end
+
+fun str_of_thm ctxt thm =
+let
+  val {prop, ...} = crep_thm (no_vars ctxt thm)
+in 
+  str_of_cterm ctxt prop
+end*}
 
 text {* 
   Again the function @{ML commas} helps with printing more than one theorem. 
@@ -171,7 +182,6 @@
 ML{*fun str_of_thms ctxt thms =  
   commas (map (str_of_thm ctxt) thms)*}
 
-
 section {* Combinators\label{sec:combinators} *}
 
 text {*