diff -r 69b5ba7518b9 -r 490fe9483c0d ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Thu Nov 03 17:53:36 2011 +0000
+++ b/ProgTutorial/First_Steps.thy	Fri Nov 04 09:29:50 2011 +0000
@@ -1251,6 +1251,8 @@
   theories, and therefore one can access the data potentially 
   indefinitely.
 
+  Move elsewhere
+
   For convenience there is an abstract layer, namely the type @{ML_type Context.generic}, 
   for treating theories and proof contexts more uniformly. This type is defined as follows
 *}