diff -r 90bee31628dc -r 18f90044c777 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Thu Mar 12 08:11:02 2009 +0100
+++ b/CookBook/FirstSteps.thy	Thu Mar 12 14:25:35 2009 +0000
@@ -169,11 +169,7 @@
 end
 
 fun str_of_thm ctxt thm =
-let
-  val {prop, ...} = crep_thm (no_vars ctxt thm)
-in 
-  str_of_cterm ctxt prop
-end*}
+  str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*}
 
 text {* 
   Again the function @{ML commas} helps with printing more than one theorem. 
@@ -533,7 +529,7 @@
 
 ML{*fun make_imp P Q tau =
 let
-  val x = Free ("x",tau)
+  val x = Free ("x", tau)
 in 
   Logic.all x (Logic.mk_implies (P $ x, Q $ x))
 end *}