--- a/ProgTutorial/FirstSteps.thy	Sat Oct 10 15:16:44 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sat Oct 10 18:25:43 2009 +0200
@@ -758,7 +758,7 @@
 end*}
 
 text {*
-  The function @{ML_ind  dest_ss in MetaSimplifier} returns a record containing all
+  The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing all
   information stored in the simpset, but we are only interested in the names of the
   simp-rules. Now you can feed in the current simpset into this function. 
   The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.