--- a/ProgTutorial/FirstSteps.thy	Sun Aug 16 21:54:47 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sun Aug 16 22:14:36 2009 +0200
@@ -508,8 +508,8 @@
   intermediate values in functions that return pairs. Suppose for example you
   want to separate a list of integers into two lists according to a
   treshold. For example if the treshold is @{ML "5"}, the list @{ML
-  "[1,6,2,5,3,4]"} should be separated to @{ML "([1,2,3,4], [6,5])"}.  You
-  can implement this function more concisely as
+  "[1,6,2,5,3,4]"} should be separated to @{ML "([1,2,3,4], [6,5])"}.  This
+  function can be implemented as
 *}
 
 ML{*fun separate i [] = ([], [])
@@ -521,9 +521,9 @@
       end*}
 
 text {*
-  where however the return value of the recursive
-  call is bound explicitly to the pair @{ML "(los, grs)" for los grs}. 
-  This function can equally be written as
+  where however the return value of the recursive call is bound explicitly to
+  the pair @{ML "(los, grs)" for los grs}. You can implement this function
+  more concisely as
 *}
 
 ML{*fun separate i [] = ([], [])
@@ -533,9 +533,9 @@
       else separate i xs |>> cons x*}
 
 text {*
-  where no explicit @{text "let"} is needed. While in this example the gain is 
-  only small, in more complicated situations the benefit of avoiding @{text "lets"} 
-  can be substantial. 
+  avoiding the explicit @{text "let"}. While in this example the gain is only
+  small, in more complicated situations the benefit of avoiding @{text "lets"}
+  can be substantial.
 
   With the combinator @{ML [index] "|->"} you can re-combine the elements from a pair.
   This combinator is defined as
@@ -1064,14 +1064,8 @@
   function that strips off the outermost quantifiers in a term.
 *}
 
-ML {*
-subst_bounds ([Free ("x", @{typ nat}), Free ("y", @{typ bool})], 
-  (Bound 1 $ Bound 0))
-*}
-
-
 ML{*fun strip_alls (Const ("All", _) $ Abs (n, T, t)) =
-    strip_alls t |>> cons (Free (n, T))
+     strip_alls t |>> cons (Free (n, T))
   | strip_alls t = ([], t) *}
 
 text {*